Security attacks on medical devices have been shown to have potential safety concerns. Because of this, stakeholders (device makers, regulators, users, etc.) have increasing interest in enhancing security in medical devices. An effective means to approach this objective is to integrate systematic security requirements elicitation and analysis into the design and evaluation of medical device software. This paper extends the sequence-based enumeration approach, a systematic approach for defining the behavior of embedded software, to analyze the requirement documents of a medical device for the purpose of eliciting security requirements. As a proof of concept, we apply our approach on a concrete case study, which shows that the extended approach is useful for identifying sequences of medical device events that might be harmful to the patient, for example because the events are initiated by an active adversary trying to use the device in a malicious way. We then show how security requirements may be formulated based on the identified threats. By exploring these sequences systematically, the developers can reliably assess what, where, and how the security threats may manifest in their system, what the safety implications are, and finally they can evaluate the resulting requirements and mitigations.

This paper presents our effort of using model-driven engineering to establish a safety-assured implementation of Patient-Controlled Analgesic (PCA) infusion pump software based on the generic PCA reference model provided by the U.S. Food and Drug Administration (FDA). The reference model was first translated into a network of timed automata using the UPPAAL tool. Its safety properties were then assured according to the set of generic safety requirements also provided by the FDA. Once the safety of the reference model was established, we applied the TIMES tool to automatically generate platform-independent code as its preliminary implementation. The code was then equipped with auxiliary facilities to interface with pump hardware and deployed onto a real PCA pump. Experiments show that the code worked correctly and effectively with the real pump. To assure that the code does not introduce any violation of the safety requirements, we also developed a testbed to check the consistency between the reference model and the code through conformance testing. Challenges encountered and lessons learned during our work are also discussed in this paper.

New research is underway at the FDA to investigate the benefits of integrating architecture analysis into safety evaluations of medical-device software. Due to the complexity in setting up testing environments for such software, the FDA is unable to conduct large-scale safety testing, instead, it must rely on other techniques to build an argument for whether the software is safe or not. The architecture analysis approach, formalized using relational algebra, is based on reconstructing abstract, yet precise, architectural views from source code to help build such arguments about safety. This paper discusses the use of the formal approach to analyze the Computer-Assisted Resuscitation Algorithm (CARA) software, which controls an infusion pump designed to provide automated assistance for transfusing blood. The results suggest that a) architecture analysis offers many insights related to software quality in general and testability (i.e., the ease of testing) and its impact on safety in particular, and b) architectural analysis results can be used to help configure static analysis tools to improve their performance for verifying safety properties.

Software testing has been commonly used in assuring the quality of database applications. It is often prohibitively expensive to manually write quality tests for complex database applications. Automated test generation techniques, such as Dynamic Symbolic Execution (DSE), have been proposed to reduce human efforts in testing database applications. However, such techniques have two major limitations: (1) they assume that the database that the application under test interacts with is accessible, which may not always be true; and (2) they usually cannot create necessary database states as a part of the generated tests.

Regulatory agencies, such as US FDA, and other third party reviewers of software have the task of comprehending apiece of software in the event of its failure. Program slicing is the preferred technique to analyze software failures. However, program slicing might yield extremely large slices and also demand that an user have intimate knowledge of the software (by specifying a slicing criterion). In this paper we propose solutions to ameliorate both of these problems. The main hypothesis of the paper is that error reports can be used to generate slicing criteria, thus allowing a third-party reviewer to use slicing without any knowledge of the system being analyzed. The first contribution of the paper is a study of how error reports can be formalized and how execution sequences (called error traces) that satisfy an error report can be identified, which can then be sliced. A primary feature of this work is that incomplete error reports could be dealt with. The second contribution of the paper is a scheme for using abstract interpretation in the generation of error traces and (potential) slicing criteria from error reports. These "abstract" error traces can be sliced, much like in dynamic/conditional slicing, with respect to the criteria generated, allowing for inputs to be used to reduce the size of slices. Furthermore, being abstract in nature, they are shorter than exact execution sequences and also allow for easier comprehension. We finally present a case study involving a medical device that illustrates how our approach can aid with program comprehension.

Post-mortem analysis - the process of tracing software failure to source code - is an important means for maintenance engineers and regulatory reviewers for establishing the cause of an error. Historically, static slicing techniques have been used for aiding post-mortem fault analysis. However, the slices obtained in this manner can often be too large and may not give a clear understanding of the code when dealing with complex reactive systems. We propose using model abstraction in conjunction with slicing to ameliorate the problem of understanding large slices. Combining slicing with abstraction provides the analyst with an integrated cognition model, leading to a better understanding of the code, and consequently more efficient error analysis. We formalize this concept through the notion of abstraction-driven slicing, and use it to develop CAdS, an automated tool to aid postmortem error detection in C programs using abstraction-driven static slicing. We list our experiences with CAdS and illustrate how it can be used to reduce effort involved in the postmortem analysis process