Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 09:15 - 09:40 at Sainte-Catherine - Session 1 Chair(s): Matteo Rossi

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 May

Displayed time zone: Eastern Time (US & Canada) change

08:40 - 10:30
Session 1FormaliSE at Sainte-Catherine
Chair(s): Matteo Rossi Politecnico di Milano
08:40
10m
Day opening
Welcome by the Chairs
FormaliSE
C: Stefania Gnesi Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
08:50
25m
Full-paper
Epistemic Model Checking of Distributed Commit Protocols with Byzantine faults
FormaliSE
Omar Bataineh NTU, Mark Reynolds The Univeristy of Western Australia
09:15
25m
Full-paper
Clock Reduction in Timed Automata while Preserving Design Parameters
FormaliSE
Beyazit Yalcinkaya Middle East Technical University, Ebru Aydin Gol Middle East Technical University
09:40
25m
Full-paper
Rigorous Design and Deployment of IoT Applications
FormaliSE
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
10:05
25m
Full-paper
Static Analysis for Worst-Case Battery Utilization
FormaliSE