Adaptive testing for specification coverage and refinement in CPS models

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.