ABSTRACT
Complex cyber-physical systems are typically hierarchically organized into multiple layers of abstraction in order to manage design complexity and provide verification tractability. Formal reasoning about such systems, therefore, necessarily involves the use of multiple modeling formalisms, verification paradigms, and concomitant tools, chosen as appropriate for the level of abstraction at which the analysis is performed.
System properties verified using an abstract component specification in one paradigm must then be shown to logically follow from properties verified, possibly using a different paradigm, on a more concrete component description, if one is to claim that a particular component when deployed in the overall system context would still uphold the system properties. But, as component specifications at one layer get elaborated into more concrete component descriptions in the next, abstraction induced differences come to the fore, which have to be reconciled in some meaningful way.
In this paper, we present our approach for providing a logical glue to tie distinct verification paradigms and reconcile the abstraction induced differences, to verify safety properties of a medical cyber-physical system. While the specifics are particular to the case example at hand-a high-level abstraction of a safety-interlock system to stop drug infusion along with a detailed design of a generic infusion pump-we believe the techniques are broadly applicable in similar situations for verifying complex cyberphysical system properties.
SYSTEM OVERVIEW
Figure 1: Overview of the closed-loop system.
As the caregiver is typically responsible for a number of patients, there may be a delay before he or she responds to an alarm. For this reason, the quality of care may be improved by a closed-loop system illustrated in Figure 1, where a safety interlock device continuously monitors the pulse oximeter readings and stops the pump once a pre-set threshold is crossed.
Figure 2: GPCA Device.
In order to contribute to this initiative by providing an archetype of system development artifacts for a Generic Patient Controlled Analgesia Infusion Pump (GPCA) system, we modeled and verified an elaborate generic PCA infusion pump, as shown in Figure 2.
MODELING
Figure 3: Infusion pump model in UPPAAL: (a) Basal infusion control (b) Bolus control.
It states that if the pump is not stopped, it delivers medication with at least the basal rate and otherwise the infusion rate is 0. Finally, the third property specifies bolus delivery. It states that, once the bolus is requested, medication is delivered at the bolus rate for the prescribed duration. The timed automata corresponding to the latter two properties are shown in Figure 3.
Figure 5: GPCA Software Architecture.
As mentioned earlier in the paper, we reused an existing model of the software (GPCA_SW). The software component (GPCA_SW) was by far the most complicated component. Hence developing it as one monolithic component was difficult to maintain as well as its verification was not scalable. Hence it was decomposed further into sub-components as shown in Figure 5.
VERIFICATION
Figure 6: Multi-model verification.
Our strategy for verifying properties over models that span multiple abstraction levels is depicted in Figure 6 using the closed-loop infusion system as the case example. The main idea is to use the notation and tools appropriate for each abstraction level, decompose the single verification problem into distinct verification tasks for each level of abstraction, and finally tie together the results in a logical fashion that is amenable to manual review.
DISCUSSION
Figure 7: Abstract PCA and Concrete GPCA High level system state mapping.
First we established a mapping between states in the abstract model of the infusion pump and the infusion modes of the concrete GPCA model, as show in Figure 7. This enables restating properties specified in terms of ow-rate constraints at the abstract level as properties in terms of the infusion modes. The different GPCA infusion modes have specific associated low-rates that can be immediately verified for conformance to low-rate constraints.
RELATED WORK
Modeling and analysis of closed-loop medical systems have been primarily studied in the context of diabetes care. Much attention is given to modeling patient physiology and design of algorithms for glucose control. However, we are not aware of any studies, where evaluation of the closed-loop system is tied to the modeling of medical devices that comprise the system.
A closed-loop safety interlock for PCA infusion, similar to the one studied in this paper, has been proposed, however, the authors do not show any analysis results. Similarly, the GPCA pump has been used in a number of case studies that involved a variety of formal methods to model different aspects of the pump behavior. In, code for a simple infusion controller has been generated from UPPAAL-verified code.
CONCLUSION
When systems are composed from sub-systems, properties of the system must be assessed based on its component properties and the composition. To reason about such systems, no single analysis and modeling method can successfully cope with all aspects of a system or its components. Hence multiple notations and formalisms are used. An approach to logically glue the diverse analysis of the system and its components is required to reason about the system properties.
In this paper, we considered compositional verification of a medical system at multiple levels of abstraction, with different formalisms used at each level. We were able to formally glue distinct verification paradigms by leveraging the system’s hierarchical architectural decomposition. We showed how properties proved for the system components at the lower levels of abstraction can be used to validate the more abstract models, ensuring that properties proved at the higher levels of abstraction remain satisfied.
While techniques used in this paper are specific to the example at hand and to the formalisms used within the case study, we believe that this work can form the basis for a general, scalable and practical approach to layered verification of properties in complex cyber-physical systems. In order to fully realize the promise of this approach, we are currently working to make the approach more systematic and eliminate the ad hoc aspects we used in this work. We are also making the approach more general, allowing more formalisms be incorporated.
Source: University of Pennsylvania
Authors: Anitha Murugesan | Oleg Sokolsky | Sanjai Rayadurgam | Michael Whalen | Mats Heimdahl | Insup Lee