Publication Details

Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming

VAŠÍČEK Ondřej, ARIAS Joaquín, FIEDOR Jan, GUPTA Gopal, HALL Brendan, KŘENA Bohuslav, LARSON Brian, VARANASI Sarat and VOJNAR Tomáš. Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming. Theory and Practice of Logic Programming, vol. 24, no. 4, 2024, pp. 844-862. ISSN 1475-3081. Available from: 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
Czech title
Brzká validace vysokoúrovňových systémových požadavků pomocí Event Kalkulu a Answer Set Programování
Type
journal article
Language
english
Authors
Vašíček Ondřej, Ing. (DITS FIT BUT)
Arias Joaquín (URJC)
Fiedor Jan, Ing., Ph.D. (DITS FIT BUT)
Gupta Gopal (UTDALLAS)
Hall Brendan
Křena Bohuslav, Ing., Ph.D. (DITS FIT BUT)
Larson Brian
Varanasi Sarat
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

requirements validation, event calculus, answer set programming, s(CASP)

Abstract

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.

Published
2024
Pages
844-862
Journal
Theory and Practice of Logic Programming, vol. 24, no. 4, ISSN 1475-3081
Publisher
Cambridge University Press
DOI
10.1017/S1471068424000280
UT WoS
001397984200018
BibTeX 
@ARTICLE{FITPUB13358,
   author = "Ond\v{r}ej Va\v{s}\'{i}\v{c}ek and Joaqu\'{i}n Arias and Jan Fiedor and Gopal Gupta and Brendan Hall and Bohuslav K\v{r}ena and Brian Larson and Sarat Varanasi and Tom\'{a}\v{s} Vojnar",
   title = "Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming",
   pages = "844--862",
   journal = "Theory and Practice of Logic Programming",
   volume = 24,
   number = 4,
   year = 2024,
   ISSN = "1475-3081",
   doi = "10.1017/S1471068424000280",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13358"
}
Back to top