Projekte pro Jahr
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.
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.
| Originalsprache | englisch |
|---|---|
| Aufsatznummer | 101254 |
| Seitenumfang | 16 |
| Fachzeitschrift | Nonlinear Analysis: Hybrid Systems |
| Jahrgang | 46 |
| DOIs | |
| Publikationsstatus | Veröffentlicht - Nov. 2022 |
Fingerprint
Untersuchen Sie die Forschungsthemen von „Adaptive testing for specification coverage and refinement in CPS models“. Zusammen bilden sie einen einzigartigen Fingerprint.Projekte
- 2 Abgeschlossen
-
ADVANCED - Adaptive Verifikation und Anomalieerkennung für komplexe Designs
Bloem, R. (Teilnehmer (Co-Investigator))
1/11/19 → 31/10/22
Projekt: Forschungsprojekt
-
Verlaesslichkeit im Internet der Dinge
Boano, C. A. (Teilnehmer (Co-Investigator)), Kubin, G. (Teilnehmer (Co-Investigator)), Bloem, R. (Teilnehmer (Co-Investigator)), Horn, M. (Teilnehmer (Co-Investigator)), Pernkopf, F. (Teilnehmer (Co-Investigator)), Zakany, N. (Teilnehmer (Co-Investigator)), Mangard, S. (Teilnehmer (Co-Investigator)), Witrisal, K. (Teilnehmer (Co-Investigator)), Römer, K. U. (Teilnehmer (Co-Investigator)), Aichernig, B. (Teilnehmer (Co-Investigator)), Bösch, W. (Teilnehmer (Co-Investigator)), Baunach, M. C. (Teilnehmer (Co-Investigator)), Tappler, M. (Teilnehmer (Co-Investigator)), Malenko, M. (Teilnehmer (Co-Investigator)), Weiser, S. (Teilnehmer (Co-Investigator)), Eichlseder, M. (Teilnehmer (Co-Investigator)), Leitinger, E. (Teilnehmer (Co-Investigator)), Grosinger, J. (Teilnehmer (Co-Investigator)), Großwindhager, B. (Teilnehmer (Co-Investigator)), Ebrahimi, M. (Teilnehmer (Co-Investigator)), Alothman Alterkawi, A. B. (Teilnehmer (Co-Investigator)), Knoll, C. (Teilnehmer (Co-Investigator)), Teschl, R. (Teilnehmer (Co-Investigator)), Saukh, O. (Teilnehmer (Co-Investigator)), Rath, M. (Teilnehmer (Co-Investigator)), Steinberger, M. (Teilnehmer (Co-Investigator)), Steinbauer-Wagner, G. (Teilnehmer (Co-Investigator)) & Tranninger, M. (Teilnehmer (Co-Investigator))
1/01/16 → 31/03/22
Projekt: Forschungsprojekt