Publication result detail

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

VAŠÍČEK, O.; ARIAS, J.; FIEDOR, J.; GUPTA, G.; HALL, B.; KŘENA, B.; LARSON, B.; VARANASI, S.; VOJNAR, T.

Original Title

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

English Title

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

Type

WoS Article

Original 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.

English 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.

Keywords

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

Key words in English

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

Authors

VAŠÍČEK, O.; ARIAS, J.; FIEDOR, J.; GUPTA, G.; HALL, B.; KŘENA, B.; LARSON, B.; VARANASI, S.; VOJNAR, T.

RIV year

2025

Released

31.07.2024

ISBN

1475-3081

Periodical

THEORY AND PRACTICE OF LOGIC PROGRAMMING

Volume

24

Number

4

State

United States of America

Pages from

844

Pages to

862

Pages count

19

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

BibTex

@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="1471-0684",
  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"
}