TY - GEN
T1 - Time-triggered conversion of guards for reachability analysis of hybrid automata
AU - Bak, Stanley
AU - Bogomolov, Sergiy
AU - Althoff, Matthias
N1 - Publisher Copyright:
© 2017, Springer International Publishing AG.
PY - 2017
Y1 - 2017
N2 - A promising technique for the formal verification of embedded and cyber-physical systems is flow-pipe construction, which creates a sequence of regions covering all reachable states over time. Flow-pipe construction methods can check whether specifications are met for all states, rather than just testing using a finite and incomplete set of simulation traces. A fundamental challenge when using flow-pipe construction on high-dimensional systems is the cost of geometric operations, such as intersection and convex hull. We address this challenge by showing that it is often possible to remove the need to perform high-dimensional geometric operations by combining two model transformations, direct time-triggered conversion and dynamics scaling. Further, we prove the overapproximation error in the conversion can be made arbitrarily small. Finally, we show that our transformation-based approach enables the analysis of a drivetrain system with up to 51 dimensions.
AB - A promising technique for the formal verification of embedded and cyber-physical systems is flow-pipe construction, which creates a sequence of regions covering all reachable states over time. Flow-pipe construction methods can check whether specifications are met for all states, rather than just testing using a finite and incomplete set of simulation traces. A fundamental challenge when using flow-pipe construction on high-dimensional systems is the cost of geometric operations, such as intersection and convex hull. We address this challenge by showing that it is often possible to remove the need to perform high-dimensional geometric operations by combining two model transformations, direct time-triggered conversion and dynamics scaling. Further, we prove the overapproximation error in the conversion can be made arbitrarily small. Finally, we show that our transformation-based approach enables the analysis of a drivetrain system with up to 51 dimensions.
UR - http://www.scopus.com/inward/record.url?scp=85029483163&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-65765-3_8
DO - 10.1007/978-3-319-65765-3_8
M3 - Conference contribution
SN - 9783319657646
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 133
EP - 150
BT - Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Proceedings
A2 - Abate, Alessandro
A2 - Geeraerts, Gilles
PB - Springer Verlag
T2 - 15th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2017
Y2 - 5 September 2017 through 7 September 2017
ER -