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

D 2024

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

VASICEK, Ondrej; Joaquin ARIAS; Jan FIEDOR; Gopal GUPTA; Brendal HALL et. al.

Základní údaje

Originální název

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

Autoři

VASICEK, Ondrej; Joaquin ARIAS; Jan FIEDOR; Gopal GUPTA; Brendal HALL; Bohuslav KRENA; Brian LARSON; Sarat chandra VARANASI a Tomáš VOJNAR

Vydání

Cambridge, Theory and Practice of Logic Programming, Volume 24 Issue 4: 40th International Conference On Logic Programming Special Issue, od s. 844-862, 19 s. 2024

Nakladatel

Cambridge University Press

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Velká Británie a Severní Irsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

Extended version of the paper available at arXiv.

Impakt faktor

Impact factor: 1.100

Kód RIV

RIV/00216224:14330/24:00139152

Organizační jednotka

Fakulta informatiky

ISSN

DOI

https://doi.org/10.1017/S1471068424000280

UT WoS

001397984200018

Klíčová slova anglicky

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

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 26. 3. 2025 00:01, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Citovat

VASICEK, Ondrej; Joaquin ARIAS; Jan FIEDOR; Gopal GUPTA; Brendal HALL; Bohuslav KRENA; Brian LARSON; Sarat chandra VARANASI a Tomáš VOJNAR. Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming. In Theory and Practice of Logic Programming, Volume 24 Issue 4: 40th International Conference On Logic Programming Special Issue. Cambridge: Cambridge University Press, 2024, s. 844-862. ISSN 1471-0684. Dostupné z: https://doi.org/10.1017/S1471068424000280.

@inproceedings{2485838,
   author = {Vasicek, Ondrej and Arias, Joaquin and Fiedor, Jan and Gupta, Gopal and Hall, Brendal and Krena, Bohuslav and Larson, Brian and Varanasi, Sarat chandra and Vojnar, Tomáš},
   address = {Cambridge},
   booktitle = {Theory and Practice of Logic Programming, Volume 24 Issue 4: 40th International Conference On Logic Programming Special Issue},
   doi = {https://doi.org/10.1017/S1471068424000280},
   keywords = {requirements validation; event calculus; answer set programming; s(CASP)},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cambridge},
   pages = {844-862},
   publisher = {Cambridge University Press},
   title = {Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming},
   url = {https://arxiv.org/abs/2408.09909},
   year = {2024}
}

TY  - CONF
ID  - 2485838
AU  - Vasicek, Ondrej - Arias, Joaquin - Fiedor, Jan - Gupta, Gopal - Hall, Brendal - Krena, Bohuslav - Larson, Brian - Varanasi, Sarat chandra - Vojnar, Tomáš
PY  - 2024
TI  - Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming
PB  - Cambridge University Press
CY  - Cambridge
KW  - requirements validation
KW  - event calculus
KW  - answer set programming
KW  - s(CASP)
UR  - https://arxiv.org/abs/2408.09909
N2  - 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.
ER  -

VASICEK, Ondrej; Joaquin ARIAS; Jan FIEDOR; Gopal GUPTA; Brendal HALL; Bohuslav KRENA; Brian LARSON; Sarat chandra VARANASI a Tomáš VOJNAR. Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming. In \textit{Theory and Practice of Logic Programming, Volume 24 Issue 4: 40th International Conference On Logic Programming Special Issue}. Cambridge: Cambridge University Press, 2024, s.~844-862. ISSN~1471-0684. Dostupné z: https://doi.org/10.1017/S1471068424000280.

Přehled o publikaci