Adaptive testing for specification coverage and refinement in CPS models

Ezio Bartocci, Roderick Bloem, Benedikt Maderbacher*, Niveditha Manjunath, Dejan Nickovic

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract

Design of correct cyber–physical systems (CPS) is of uttermost importance for safety-critical applications. This crucial yet extremely challenging property is often addressed in practice by simulation-based methods. The simulation activity can be made more systematic and rigorous by using formal specifications to express requirements and guide the testing of the system.

In this paper, we develop a procedure for generating tests from formal specifications given in Signal Temporal Logic (STL), a declarative language used to express CPS requirements. The proposed test generation method is adaptive with the aim at achieving specification coverage. We devise to this goal cooperative reachability games, which we enhance with numerical optimization to facilitate exercising various parts of specifications. The resulting approach is effective in finding specification violations, but also in increasing confidence (via coverage) that the specification is satisfied. In the latter case, we also propose a method for automatically refining the specification into its part that is actually implemented, thus gaining additional insight into the system-under-test.
Original languageEnglish
Article number101254
Number of pages16
JournalNonlinear Analysis: Hybrid Systems
Volume46
DOIs
Publication statusPublished - Nov 2022

Fingerprint

Dive into the research topics of 'Adaptive testing for specification coverage and refinement in CPS models'. Together they form a unique fingerprint.

Cite this