Early Validation of High-level System Requirements with Event Calculus and Answer Set Programming
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866929463564959744 |
|---|---|
| author | Vašíček, Ondřej Arias, Joaquin Fiedor, Jan Gupta, Gopal Hall, Brendan Křena, Bohuslav Larson, Brian Varanasi, Sarat Chandra Vojnar, Tomáš |
| author_facet | Vašíček, Ondřej Arias, Joaquin Fiedor, Jan Gupta, Gopal Hall, Brendan Křena, Bohuslav Larson, Brian Varanasi, Sarat Chandra Vojnar, Tomáš |
| contents | 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$-$a 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_09909 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Early Validation of High-level System Requirements with Event Calculus and Answer Set Programming Vašíček, Ondřej Arias, Joaquin Fiedor, Jan Gupta, Gopal Hall, Brendan Křena, Bohuslav Larson, Brian Varanasi, Sarat Chandra Vojnar, Tomáš Logic in Computer Science Software Engineering 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$-$a 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. |
| title | Early Validation of High-level System Requirements with Event Calculus and Answer Set Programming |
| topic | Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2408.09909 |