Hybrid systems are a powerful formalism for modeling cyber- physical systems. Reachability analysis is a general method for check- ing 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 reachable 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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||A Semantic Account of Rigorous Simulation|
|Data di pubblicazione:||2018|
|Appare nelle tipologie:||02.01 - Contributo in volume (Capitolo o saggio)|