A Conformance Review Strategy for Regulating Safety-Critical Software.

slicing;abstraction;usage model;formal methods;regulatory agencies

Jetley, Raoul Praful ; Dr. S. Purushothaman Iyer, Committee Chair,Dr. Laurie Williams, Committee Member,Dr. Matthias Stallmann, Committee Member,Dr. Alexander Dean, Committee Member,Jetley, Raoul Praful ; Dr. S. Purushothaman Iyer ; Committee Chair ; Dr. Laurie Williams ; Committee Member ; Dr. Matthias Stallmann ; Committee Member ; Dr. Alexander Dean ; Committee Member

University:North Carolina State University

关键词: slicing;    abstraction;    usage model;    formal methods;    regulatory agencies;   

Others  :  https://repository.lib.ncsu.edu/bitstream/handle/1840.16/5195/etd.pdf?sequence=1&isAllowed=y

美国|英语

来源: null

【 摘 要 】

Safety is an important concern for software used in life-critical systems such as air transport, nuclear power and medical devices. The critical nature of these systems necessitates that the software used therein be reliable and free of errors. It becomes imperative, therefore, to have a stringent review process in place to ascertain the correctness of the software and to ensure that it meets all requirements and standards. Regulatory agencies encourage the use of formal methods based techniques in the development of safety critical software. However, most manufacturers are reluctant to use these techniques, citing them as too complex and time consuming. As a result, (potentially life-threatening) errors are often not discovered until the software is already on the market. When such an error is eventually discovered, it becomes essential to trace the failure to its exact source in the implementation and to assure that the error correction restores the overall safety and effectiveness of the device. In this dissertation, we present how efficient premarket and postmarket reviews of designs and implementations can be carried out using formal methods based techniques, to enable the process of reviewing software in safety-critical devices. To facilitate premarket conformance reviews, we introduce the notion of usage models -- standardized formal models that serve as design templates. We present an approach to conformance checking of safety-critical software through formal verification and automated test case sequences derived from these standardized models. To provide for efficient postmarket reviews, we establish a methodology based on integrating program slicing with model abstraction to trace software failures to their root cause. We formalize this methodology by presenting an iterative algorithm for abstraction-driven slicing and realize this algorithm through the implementation of the CAdS -- a forensic analysis tool for C programs. We provide case studies involving typical medical device software to illustrate the various concepts involved and present results from these studies to gauge the effectiveness of our proposed approach.