2015/11/03 by Jeroen J. A. Keiren, Keiren, Jeroen J. A., Martijn Klabbers +1
Computer Science · Engineering · #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Safety Systems Engineering in Autonomy
paper · doi:10.14279/tuj.eceasst.53.793
openalex publication_date 2024/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/15
In this paper we advocate that formal verification should bea part of the development of a communication standard;in a short period of time issues areuncovered that have been in the standard for a number of years, and allsubtleties in the correctness of the protocol are understood. We model and verify the session setup protocolthat is part of the IEEE 11073-20601:2008 standard for communication betweenpersonal health devices.We identify a number of issues present in the standards document.Discussion with a member of the standards committee unveiled that most, but notall, of the identified issues are fixed in the IEEE 11073-20601:2010 version ofthe standard.In addition, the correctness of the protocol, including the fixes, is assessed.For this, properties of the session setup protocol are formulated, and usingthe model checker mCRL2 it is verified whether the model satisfies theseproperties.We show that the session setup protocol is flawed, and propose a straightforwardway to fix this issue.