Formal patterns for medical device safety

Sun, Mu

Permalink

https://hdl.handle.net/2142/46661 Copy

Description

Title

Formal patterns for medical device safety

Author(s)

Sun, Mu

Issue Date

2014-01-16T17:58:02Z

Director of Research (if dissertation) or Advisor (if thesis)

Sha, Lui R.

Doctoral Committee Chair(s)

Sha, Lui R.

Committee Member(s)

• Meseguer, José
• Agha, Gul A.
• Jetley, Raoul

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• Formal Methods
• Design Patterns
• Medical Systems

Abstract

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.

Graduation Semester

2013-12

Permalink

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

Copyright and License Information

Copyright 2013 Mu Sun

Owning Collections