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. Modelling the PCA Pump Requirements in EC under s(CASP) 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
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 diference of total drug delivered at the start and at the end of a bolus (lines 17-20).
Validating Consistency of Use/Exception Cases and the Requirements 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 diferent 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).
3 ?- holdsIn(basal_delivery_enabled,
4 happens(patient_bolus_delivery_started,
5 not_happens(patient_bolus_denied,
6 initiallyP(vtbi(VTBI)), happens(patient_bolus_completed,
7 holdsAt(patient_bolus_drug_delivered(VTBI),
8 happens(basal_delivery_started,
9 holdsAfter(basal_delivery_enabled,
60, 120),
120),
120),
T2),
T2),
T2),
T2).
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.
Results of Experimental Evaluation 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).
Techniques Used to Empower s(CASP) Reasoning 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 [
Our future work involves improving s(CASP) in order to make it more eficient 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 [