Detail publikace

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 a VOJNAR Tomáš. Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming. Theory and Practice of Logic Programming, roč. 24, č. 4, 2024, s. 844-862. ISSN 1475-3081. Dostupné z: 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
Název česky
Brzká validace vysokoúrovňových systémových požadavků pomocí Event Kalkulu a Answer Set Programování
Typ
článek v časopise
Jazyk
angličtina
Autoři
Vašíček Ondřej, Ing. (UITS FIT VUT)
Arias Joaquín (URJC)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Gupta Gopal (UTDALLAS)
Hall Brendan
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
Larson Brian
Varanasi Sarat
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
URL
Klíčová slova

validace požadavků, event kalkulus, answer set programování, s(CASP)

Abstrakt

Tento článek navrhuje novou metodiku pro brzkou validaci vysokoúrovňových požadavků na kyberneticko-fyzikální systémy s cílem zlepšit jejich kvalitu a tím snížit pravděpodobnost, že se chyby ve specifikaci rozšíří do pozdějších fází vývoje, kde je jejich oprava mnohem nákladnější. Článek představuje transformaci reálné specifikace požadavků na lékařské zařízení --- pumpu pro pacientem řízenou analgesií (PCA) --- do modelu v Event Kalkulu, který je následně vyhodnocen pomocí Answer Set Programování a nástroje s(CASP). Vyhodnocování pomocí nástroje s(CASP) umožnilo deduktivní i abduktivní uvažování o specifikované funkčnosti PCA pumpy na konceptuální úrovni s minimálními vlivy závislými na implementaci nebo návrhu a vedlo k plně automatizované detekci porušení kritických bezpečnostních vlastností. Článek dále pojednává o problémech škálovatelnosti a neterminace, kterým bylo třeba při vyhodnocování čelit, a o technikách navržených k jejich (částečnému) řešení. Nakonec jsou uvedena možná vylepšení nástroje s(CASP), aby se překonala jeho omezení při vyhodnocování, která stále přetrvávají, a také aby se zvýšila jeho vyjadřovací schopnost.

Rok
2024
Strany
844-862
Časopis
Theory and Practice of Logic Programming, roč. 24, č. 4, ISSN 1475-3081
Vydavatel
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"
}
Nahoru