Options
A model template for reachability-based containment checking of imprecise observations in timed automata
Citation Link: https://doi.org/10.15480/882.13769
Publikationstyp
Journal Article
Date Issued
2024-09-19
Sprache
English
Author(s)
Lehmann, Sascha
TORE-DOI
Journal
Citation
Software and Systems Modeling (in Press): (2024)
Publisher DOI
Scopus ID
Publisher
Springer
Verifying safety requirements by model checking becomes increasingly important for safety-critical applications. For the validity of such proof in practice, the model needs to capture the actual behavior of the real system, which could be tested by containment checks of real observation traces. Basic equivalence checks, however, are not applicable if the system is only partially or imprecisely observable, if the model abstracts from explicit states with symbolic semantics, or if the checks are not expressible in the logics supported by a model checker. In this article, we solve the problem of observation containment checking in timed automata via reachability checking on tester systems. We introduce the logic SRL (sequence reachability logic) to express observations as sequences of delayed reachability properties. Through SBLL (introduced by Aceto et al.) as intermediate logic, we synthesize a set of matcher model templates for partial and imprecise observations and further extend these templates for the case of limited state accessibility in a model. For the obtained matching traces, we define the back-transformation into the original model domain and formally prove the correctness of the transformation. We implemented the observation matching approach, and apply it to a set of 7 demo and 3 case study models with different levels of observability. The results show that all positive and negative observations are correctly classified, and that the most advanced matcher model instance still offers average run times between 0.1 and 1 s in all but 3 scenarios.
Subjects
Containment checking | Model transformation | Observation matching | Reachability problem | Timed automata
DDC Class
004: Computer Sciences
620: Engineering
519: Applied Mathematics, Probabilities
Publication version
publishedVersion
Loading...
Name
s10270-024-01205-w.pdf
Type
Main Article
Size
1.93 MB
Format
Adobe PDF