Early validation of specifications describing requirements placed on cyber-physical systems (CPSs) under development is essential to avoid costly errors in later stages of the development, especially when the systems undergo certification. However, there is a lack of suitable automated tools and techniques for this purpose. A crucial need here is that of a small semantic gap between the requirements and the formalism used to model them for the purposes of validation. As described by [2], Event Calculus (EC) is a formalism suitable for commonsense reasoning. The semantic gap between a requirements specification and its EC encoding is near-zero because its semantics follows how a human would think of the requirements. Using Answer Set Programming (ASP) [3] and the s(CASP) [4] system for goal-directed reasoning in EC, the work [5] has demonstrated the versatility of EC for modelling and reasoning about CPSs.
In this work, we develop a model of the core operation of the PCA pump [6]-a real safety-critical device that automatically delivers pain relief drugs into the blood stream of a patient-in order to assess, demonstrate, and improve the practical capabilities (and current limitations) of the EC+s(CASP) approach. The model operates in a way similar to an early prototype of the system and, thus, can be used to reason about its behaviour. However, due to the nature of EC, the behaviour of the model is very close to what the requirements themselves describe.
The transformation of the requirements specification of the PCA pump into an EC representation implemented in s(CASP) was done manually. The requirements specification and all the source codes of its s(CASP) representation can be found at https://github.com/ovasicek/pca-pump-ec-artifacts/. The below is a brief, illustrative overview of s(CASP) code for the delivery of a patient bolus (one of the features of the pump), which 4th Workshop on Goal-directed Execution of Answer Set Programs (GDE'24), October 12, 2024
is an extra dose of drug delivered upon the patient's request. We define events that start and end the delivery of the bolus which is represented by a state fluent (lines 1-4). The total amount of drug delivered to the patient and how the amount increases during the bolus is represented by a continuous fluent and a trajectory (lines 6-10). And finally, the bolus stops automatically once the right amount of drug (so called VTBI) is delivered which is represented by an event triggered based on the drug delivered during the ongoing bolus (lines 12-15). A new continuous fluent and trajectory are used to represent the volume of drug delivered by a bolus counting from zero instead of computing the difference of total drug delivered at the start and at the end of a bolus (lines 17-20).
1 fluent(patient_bolus_delivery_enabled). 2 event(patient_bolus_delivery_started). event(patient_bolus_delivery_stopped).
3 initiates(patient_bolus_delivery_started, patient_bolus_delivery_enabled, T). 4 terminates(patient_bolus_delivery_stopped, patient_bolus_delivery_enabled, T).
The first validation method that we propose is a way to check the consistency between the behaviour defined by the requirements specification and the use cases (UC) and exception cases (ExC) based on which the requirements were created (or, in general, checking consistency of the behaviour against any scenarios defined at a different level of the specification) by, essentially, simulating the UC/ExC. This is done by transforming the UC/ExC into an EC narrative and forming a query based on the UC/ExC and its post-conditions. If running the query on the narrative using s(CASP) fails, then we have found an inconsistency. Using this technique we were able to identify a number of such inconsistencies in the PCA pump specification. A simplified example of such a narrative and query for UC2: Patient-Requested Bolus is shown below. The use case specifies the delivery of a patient requested bolus which is requested during basal delivery (the baseline delivery mode), is not denied by the pump, and the pump goes back to basal delivery after the bolus finishes. Lines 1-2 specify the input events which occur in the narrative, and lines 3-9 define the query to be checked. Full implementation of UC2 can be found in uc2.pl.
1 happens(start_button_pressed, 60).
2 happens(patient_bolus_requested, 120). Validating the Requirements wrt. General Properties The second validation method that we propose is a way to check whether the requirements specification satisfies general properties, such as that the system should not allow an overdose of the patient or that the system should respond to an event within a given time limit. This is done by representing a general property as an s(CASP) query and checking that query on suitable narratives. In this way, we were able to detect that the patient can be overdosed by the PCA pump in certain specific narratives, which is a safety property violation caused by a missing requirement. We were further able to leverage the abductive reasoning capabilities of s(CASP) in order to generalize the narrative on which the property is being checked. In our case of checking the possibility of an overdose, we were able to abduce the parameters of an overdose (what volume of drug is allowed over what time period) and, subsequently, detect the possibility of an overdose in the "sunny day" narrative of UC2 in which the overdose does not directly occur otherwise.
We have simulated all relevant UCs and ExCs from the PCA pump specification and checked the possibility of an overdoes of the patient. Some of the cases appear in multiple variants of the narrative and we aggregate the measurements of variants of the same case that led to the same result to save space. Implementations of all experiments can be found in the narratives_and_queries folder. Table 1 shows selected representative results of simulating UCs and ExCs. All UCs were simulated successfully, but quite a few ExCs failed. This has led to the discovery of a number of issues in the specification, such as inconsistencies in alarm responses or defined constants. Table 2 shows results and execution times of querying overdose on variants of ExC13 (implemented in overdose-ec13b.pl and similar) and of using abduction on UC2. Execution of the overdose queries takes much longer than the simulation queries from Table 1 due to the higher complexity of the overdose query. However, the abductive queries are the slowest ones due to the higher complexity of abduction in general but also due to the limitations of its current implementation in s(CASP).
We further present a number of challenges encountered during the translation of the requirements to EC encoded in s(CASP) and during the subsequent evaluation, based on deductive as well as abductive reasoning, which was often too costly or non-terminating. We have applied and, in multiple cases, also newly developed various techniques that helped us resolve many of these challenges. These include extensions of the axiomatization of the EC (in a similar way as [7]) and special ways of translating certain parts of the specifications in order to avoid non-termination, in particular when dealing with certain trajectories. Further, we present an original approach to abductive reasoning in s(CASP) with incrementally refined abduced values in order to assure consistency of the abduced values whenever abduction on the same value is used multiple times in the reasoning tree. Next, we proposed a mechanism for caching evaluations (failure-tabling and tabling of ground sub-goal success) of selected predicates (in a similar way as mode-directed tabling [8,9]) that was added into s(CASP) as a prototype leading to a significant increase in performance. We also describe a way of separating the reasoning about the trigger and the effect of certain complexity-inducing triggered events into multiple reasoning runs where each run produces new facts to be used in the subsequent ones, which reduces their performance impact.
Our work demonstrated that EC can be used to model the requirements specification of a non-trivial, real-life cyber-physical system in s(CASP) and the reasoning involved can lead to discovering issues in the requirements while producing valuable evidence towards their validation. Indeed, the work resulted in the discovery of a number of issues in the PCA pump specification, which we have discussed and confirmed with the authors of the specification. Our future work involves improving s(CASP) in order to make it more efficient and to reduce the number of non-termination issues, and making our approach more general and practically usable, in particular targeting the transformation phase by introducing a more structured specification language such as [10].