TY - GEN
T1 - A formal pattern architecture for safe medical systems
AU - Sun, Mu
AU - Meseguer, José
AU - Sha, Lui
N1 - Funding Information:
We would like to thank all the people of the UIUC MD PnP group and the UIUC Maude Seminar group who have provided many valuable insights and suggestions towards improving this work. This work was supported in part by ONR grant N000140810896 and by NSF grants 0720482 and 0834709.
Funding Information:
Acknowledgements. We would like to thank all the people of the UIUC MD PnP group and the UIUC Maude Seminar group who have provided many valuable insights and suggestions towards improving this work. This work was supported in part by ONR grant N000140810896 and by NSF grants 0720482 and 0834709.
PY - 2010
Y1 - 2010
N2 - Design patterns have demonstrated major practical uses for cost savings and modular design in software engineering. For safety-critical systems, however, such patterns should also provide formal guarantees that critical safety properties are met. We leverage the power of rewriting logic and parameterization available in Real-Time Maude to add a formal basis for analysis of a novel safety pattern for medical devices. We demonstrate practicality and applicability of our pattern by instantiating it to a pacemaker specification, and we validate our pattern by verifying the safety invariant in the pacemaker instantiation.
AB - Design patterns have demonstrated major practical uses for cost savings and modular design in software engineering. For safety-critical systems, however, such patterns should also provide formal guarantees that critical safety properties are met. We leverage the power of rewriting logic and parameterization available in Real-Time Maude to add a formal basis for analysis of a novel safety pattern for medical devices. We demonstrate practicality and applicability of our pattern by instantiating it to a pacemaker specification, and we validate our pattern by verifying the safety invariant in the pacemaker instantiation.
UR - http://www.scopus.com/inward/record.url?scp=78349232362&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78349232362&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-16310-4_11
DO - 10.1007/978-3-642-16310-4_11
M3 - Conference contribution
AN - SCOPUS:78349232362
SN - 3642163092
SN - 9783642163098
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 157
EP - 173
BT - Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers
T2 - 8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010
Y2 - 20 March 2010 through 21 March 2010
ER -