Currently, communication protocols for medical devices are being developed for the IEEE 1073.2 standard. The protocol description in its draft remote control package consists of a collection of intended behaviors in terms of MSCs. We have contributed to actually constructing the protocol, ranging from determining an hMSC for these MSCs, via synthesizing process implementations, to integrating it with the basic underlying IEEE 1073.2 protocol. In this paper we report on the non-local choice problems we encountered. We present a practical solution (i.e., an implementation) which on the one hand is close to the behavior specified in the hMSC, and on the other hand meets correctness properties such as deadlock freedom. These properties have been checked using the Spin model checker. We also give some directions for generalizing and extending this work.
|Title of host publication||System Analysis and Modelling (4th International SDL and MSC Workshop, SAM'04, Ottawa, Canada, June 1-4, 2004, Revised Selected Papers)|
|Editors||D. Amyot, A.W. Williams|
|Place of Publication||Berlin|
|Publication status||Published - 2005|
|Name||Lecture Notes in Computer Science|