Formal patterns for medical device safety

Formal methods have revolutionized software reliability and safety, and design patterns has revolutionized software reusability and modularity. However, the preciseness required for formal methods and the flexibility inherent in design patterns has rendered these two concepts somewhat disjoint and applied to different application domains. Currently, new uses of software in medical device plug-and-play systems has pointed to a need for creating systems that are both flexible and safe. In this dissertation, we describe significant advancements towards the development of formal patterns to achieve greater assurance about medical device safety. We consider three levels of safety and associated case studies in the medical device domain: device interface safety, medical requirement safety, and network safety. For device interface safety we look at various button-related faults and describe pattern solutions for addressing each fault. For medical requirement safety we focus on a particular class of stress-relax safety and present the Command-Shaper pattern to address this. Finally, in the network safety area we look at the particular case of message loss and describe an active message repeater pattern. For each of these patterns: (i) we formally define them in the Maude rewriting logic framework; (ii) we show their correctness by rigorously proving the required properties based on their rewriting logic specification; and (iii) we also show practicality of each pattern with execution, model checking, and emulation.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2014

Author dc:creator

• Sun, Mu

Contributors dc:contributor

• Sha, Lui R.
• Meseguer, José
• Agha, Gul A.
• Jetley, Raoul

• Formal Methods
• Design Patterns
• Medical Systems

Statement dc:rights

• Copyright 2013 Mu Sun

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/46661

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/46661