Files in this item

FilesDescriptionFormat

application/pdf

application/pdfMu_Sun.pdf (1MB)
(no description provided)PDF

Description

Title:Formal patterns for medical device safety
Author(s):Sun, Mu
Director of Research:Sha, Lui R.
Doctoral Committee Chair(s):Sha, Lui R.
Doctoral Committee Member(s):Meseguer, José; Agha, Gul A.; Jetley, Raoul
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(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.
Issue Date:2014-01-16
URI:http://hdl.handle.net/2142/46661
Rights Information:Copyright 2013 Mu Sun
Date Available in IDEALS:2014-01-16
Date Deposited:2013-12


This item appears in the following Collection(s)

Item Statistics