{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/46661"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/46661","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Formal patterns for medical device safety","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Sun, Mu"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Sha, Lui R.","Meseguer, José","Agha, Gul A.","Jetley, Raoul"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2014,"date_issued":"2014-01-16T17:58:02Z","date_published":"2014-01-16T17:58:02Z","updated_at":"2026-07-22T22:25:36Z","subjects":["Formal Methods","Design Patterns","Medical Systems"],"languages":["en"],"rights":["Copyright 2013 Mu Sun"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/46661","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Sha, Lui R.","Meseguer, José","Agha, Gul A.","Jetley, Raoul"]},{"key":"dc:creator","label":"Author","values":["Sun, Mu"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2014-01-16T17:58:02Z","2013-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Formal Methods","Design Patterns","Medical Systems"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2013 Mu Sun"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/46661"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Item withdrawn by Laura Spradlin (lspradl2@illinois.edu) on 2013-12-04T20:41:00Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Sun_Mu.pdf: 1380737 bytes, checksum: b367cd1465d1b2715c3ef057128602b9 (MD5)","Made available in DSpace on 2014-01-16T17:58:02Z (GMT). No. of bitstreams: 2 Mu_Sun.pdf: 1384194 bytes, checksum: 55e88009e8c509574d2abf89157cd77c (MD5) license.txt: 4053 bytes, checksum: dfb70dc18a7dcd86a30dd92f689e8ad0 (MD5)"]},{"key":"dc:title","label":"Title","values":["Formal patterns for medical device safety"]}]}],"canonical_facts":{"dc:contributor":["Sha, Lui R.","Meseguer, José","Agha, Gul A.","Jetley, Raoul"],"dc:creator":["Sun, Mu"],"dc:date":["2014-01-16T17:58:02Z","2013-12"],"dc:description":["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.","Item withdrawn by Laura Spradlin (lspradl2@illinois.edu) on 2013-12-04T20:41:00Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Sun_Mu.pdf: 1380737 bytes, checksum: b367cd1465d1b2715c3ef057128602b9 (MD5)","Made available in DSpace on 2014-01-16T17:58:02Z (GMT). No. of bitstreams: 2 Mu_Sun.pdf: 1384194 bytes, checksum: 55e88009e8c509574d2abf89157cd77c (MD5) license.txt: 4053 bytes, checksum: dfb70dc18a7dcd86a30dd92f689e8ad0 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/46661"],"dc:language":["en"],"dc:rights":["Copyright 2013 Mu Sun"],"dc:subject":["Formal Methods","Design Patterns","Medical Systems"],"dc:title":["Formal patterns for medical device safety"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:36Z"}