Abstract
In this paper we advocate that formal verification should be a part of the development of a communication standard; in a short period of time issues are uncovered that have been in the standard for a number of years, and all subtleties in the correctness of the protocol are understood. We model and verify the session setup protocol that is part of the IEEE 11073-20601:2008 standard for communication between personal 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 not all, of the identified issues are fixed in the IEEE 11073-20601:2010 version of the standard. In addition, the correctness of the protocol, including the fixes, is assessed. For this, properties of the session setup protocol are formulated, and using the model checker mCRL2 it is verified whether the model satisfies these properties. We show that the session setup protocol is awed, and propose a straightforward way to fix this issue.
| Original language | English |
|---|---|
| Title of host publication | 12th International Workshop on Automated Verification of Critical Systems (AVoCS, Bamberg, Germany, September 18-20, 2012) |
| Editors | G. Lüttgen, S. Merz |
| Publisher | ECEASST |
| Pages | 1-16 |
| Publication status | Published - 2012 |
| Event | 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012) - Bamberg, Germany Duration: 18 Sept 2012 → 20 Sept 2012 Conference number: 12 |
Publication series
| Name | Electronic Communications of the EASST |
|---|---|
| Volume | 53 |
| ISSN (Print) | 1863-2122 |
Conference
| Conference | 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012) |
|---|---|
| Abbreviated title | AVoCS 2012 |
| Country/Territory | Germany |
| City | Bamberg |
| Period | 18/09/12 → 20/09/12 |