Hybrid systems are a powerful formalism for modeling cyber-physical systems. Reachability analysis is a general method for checking safety properties, especially in the presence of uncertainty and non-determinism. Rigorous simulation is a convenient tool for reachability analysis of hybrid systems. However, to serve as proof tool, a rigorous simulator must be correct wrt a clearly defined notion of reachability,which captures what is intuitively eachable in finite time. As a step towards addressing this challenge, this paper presents a rigorous simulator in the form of an operational semantics and a specification in the form of a denotational semantics. We show that, under certain conditions about the representation of enclosures, the rigorous simulator is correct. We also show that finding a representation satisfying these assumptions is non-trivial.
Titolo: | A Semantic Account of Rigorous Simulation |
Autori: | |
Data di pubblicazione: | 2018 |
Handle: | http://hdl.handle.net/11567/914208 |
ISBN: | 978-3-319-95245-1 978-3-319-95246-8 |
Appare nelle tipologie: | 02.01 - Contributo in volume (Capitolo o saggio) |
File in questo prodotto:
File | Descrizione | Tipologia | |
---|---|---|---|
EAL17.pdf | Pre-print articolo principale | Documento in Post-print | Open Access Visualizza/Apri |