Early Validation of High-level Requirements on Cyber-Physical Systems

TL;DR

The paper tackles early validation of high-level CPS requirements by translating natural-language specifications into Event Calculus (EC) and leveraging the grounding-free, abductive ASP solver s(CASP) for continuous-time reasoning. It demonstrates, through a PCA pump case study, how EC+s(CASP) can detect inconsistencies with use cases and uncover safety-property gaps, while producing explainable proofs of the reasoning. The work also presents practical techniques to mitigate non-termination and scalability challenges, such as extending EC axioms, refining abduction, caching, and dividing complex reasoning into manageable runs. It argues for semi-automated transformation of requirements to EC (potentially aided by MIDAS or controlled NLP models) to broaden industrial applicability while maintaining safety and explainability.

Abstract

The overarching, broad topic of my research are advancements in the area of safety-critical, cyber-physical systems (CPS) development with emphasis on validation and verification. The particular focus of my research is the early validation of high-level requirements on CPS. My current approach for tackling this problem is transforming the requirements into Event Calculus and subsequently reasoning about them using ASP solvers such as the grounding-free s(CASP). Below, I discuss my research, its current state, and the open issues that are still left to tackle. The first results of my work will be presented in a paper that was accepted for ICLP'24, which is my first paper in this area.