Publication Details
Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming
ARIAS, J.
Fiedor Jan, Ing., Ph.D. (DITS)
GUPTA, G.
HALL, B.
Křena Bohuslav, Ing., Ph.D. (DITS)
LARSON, B.
VARANASI, S.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
requirements validation, event calculus, answer set programming, s(CASP)
This paper proposes a new methodology for early validation of high-level
requirements on cyber-physical systems with the aim of improving their quality
and, thus, lowering chances of specification errors propagating into later stages
of development where it is much more expensive to fix them. The paper presents
a transformation of a real-world requirements specification of a medical
device---the Patient-Controlled Analgesia (PCA) Pump---into an Event Calculus
model that is then evaluated using Answer Set Programming and the s(CASP) system.
The evaluation under s(CASP) allowed deductive as well as abductive reasoning
about the specified functionality of the PCA pump on the conceptual level with
minimal implementation or design dependent influences and led to fully
automatically detected nuanced violations of critical safety properties. Further,
the paper discusses scalability and non-termination challenges that had to be
faced in the evaluation and techniques proposed to (partially) solve them.
Finally, ideas for improving s(CASP) to overcome its evaluation limitations that
still persist as well as to increase its expressiveness are presented.
@article{BUT196476,
author="VAŠÍČEK, O. and ARIAS, J. and FIEDOR, J. and GUPTA, G. and HALL, B. and KŘENA, B. and LARSON, B. and VARANASI, S. and VOJNAR, T.",
title="Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming",
journal="Theory and Practice of Logic Programming",
year="2024",
volume="24",
number="4",
pages="844--862",
doi="10.1017/S1471068424000280",
issn="1475-3081",
url="https://www.cambridge.org/core/services/aop-cambridge-core/content/view/E0C3F905117E7F793E09C5A355B34BB2/S1471068424000280a.pdf/early-validation-of-high-level-system-requirements-with-event-calculus-and-answer-set-programming.pdf"
}