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.
PDF
download
878987797
028-85220240
