Clock Reduction in Timed Automata while Preserving Design Parameters
Timed automata (TA) are widely used to model and verify real-time systems. In a TA, the real valued variables, called clocks, measure the time passed between events. The verification of TA is exponential in the number of clocks. That constitutes a bottleneck for its application in large systems. To address this issue, we propose a novel clock reduction method. We aim at reducing the number of clocks by developing a position (location and transition) based mapping for clocks. Motivated by that the locations and transitions of the automaton reflect the modeled system’s physical properties and design parameters; the proposed method changes the clock constraints based on their positions to reduce the total number of clocks. To guarantee correctness, we prove that the resulting automaton is timed bisimilar to the original one. Finally, we present empirical results for the solution, which show that the proposed method significantly reduces the clock count without changing design parameters of the system.
Mon 27 MayDisplayed time zone: Eastern Time (US & Canada) change
08:40 - 10:30
Session 1FormaliSE at Sainte-Catherine
Chair(s): Matteo Rossi Politecnico di Milano
|Welcome by the Chairs|
C: Stefania Gnesi Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
|Epistemic Model Checking of Distributed Commit Protocols with Byzantine faults|
Omar Bataineh NTU, Mark Reynolds The Univeristy of Western Australia
|Clock Reduction in Timed Automata while Preserving Design Parameters|
Beyazit Yalcinkaya Middle East Technical University, Ebru Aydin Gol Middle East Technical University
|Rigorous Design and Deployment of IoT Applications|
Ajay Krishna Inria Grenoble, France, Michel Le Pallec Nokia Bell Labs, Radu Mateescu INRIA, Ludovic Noirie Nokia Bell Labs, Gwen Salaün University of Grenoble Alpes
|Static Analysis for Worst-Case Battery Utilization|
Dmitry Ivanov TomTom, Sibylle Schupp