TY - GEN
T1 - Verification and Performance Evaluation of Timed Game Strategies
AU - David, Alexandre
AU - Fang, Huixing
AU - Larsen, Kim Guldstrand
AU - Zhang, Zhengkui
PY - 2014
Y1 - 2014
N2 - Control synthesis techniques, based on timed games, derive strategies to ensure a given control objective, e.g., time-bounded reachability. Model checking verifies correctness properties of systems. Statistical model checking can be used to analyse performance aspects of systems, e.g., energy consumption. In this work, we propose to combine these three techniques. In particular, given a strategy synthesized for a timed game and a given control objective, we want to make a deeper examination of the consequences of adopting this strategy. Firstly, we want to apply model checking to the timed game under the synthesized strategy in order to verify additional correctness properties. Secondly, we want to apply statistical model checking to evaluate various performance aspects of the synthesized strategy. For this, the underlying timed game is extended with relevant price and stochastic information. We first explain the principle of translating a strategy produced by Uppaal-tiga into a timed automaton, thus enabling the deeper examination. However, our main contribution is a new extension of Uppaal that automatically synthesizes a strategy of a timed game for a given control objective, then verifies and evaluates this strategy with respect to additional properties. We demonstrate the usefulness of this new branch of Uppaal using two case-studies.
AB - Control synthesis techniques, based on timed games, derive strategies to ensure a given control objective, e.g., time-bounded reachability. Model checking verifies correctness properties of systems. Statistical model checking can be used to analyse performance aspects of systems, e.g., energy consumption. In this work, we propose to combine these three techniques. In particular, given a strategy synthesized for a timed game and a given control objective, we want to make a deeper examination of the consequences of adopting this strategy. Firstly, we want to apply model checking to the timed game under the synthesized strategy in order to verify additional correctness properties. Secondly, we want to apply statistical model checking to evaluate various performance aspects of the synthesized strategy. For this, the underlying timed game is extended with relevant price and stochastic information. We first explain the principle of translating a strategy produced by Uppaal-tiga into a timed automaton, thus enabling the deeper examination. However, our main contribution is a new extension of Uppaal that automatically synthesizes a strategy of a timed game for a given control objective, then verifies and evaluates this strategy with respect to additional properties. We demonstrate the usefulness of this new branch of Uppaal using two case-studies.
U2 - 10.1007/978-3-319-10512-3_8
DO - 10.1007/978-3-319-10512-3_8
M3 - Article in proceeding
SN - 978-3-319-10511-6
VL - 8711
T3 - Lecture Notes in Computer Science
SP - 100
EP - 114
BT - Formal Modeling and Analysis of Timed Systems
A2 - Legay, Axel
A2 - Bozga, Marius
PB - Springer
ER -