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
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

Formalise-2019-papers
08:40 - 10:30: FormaliSE 2019 - Session 1 at Sainte-Catherine
Chair(s): Matteo RossiPolitecnico di Milano
Formalise-2019-papers08:40 - 08:50
Day opening
Stefania GnesiIstituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
Formalise-2019-papers08:50 - 09:15
Full-paper
Omar BatainehNTU, Mark ReynoldsThe Univeristy of Western Australia
Formalise-2019-papers09:15 - 09:40
Full-paper
Beyazit YalcinkayaMiddle East Technical University, Ebru Aydin GolMiddle East Technical University
Formalise-2019-papers09:40 - 10:05
Full-paper
Ajay KrishnaInria Grenoble, France, Michel Le PallecNokia Bell Labs, Radu MateescuINRIA, Ludovic NoirieNokia Bell Labs, Gwen SalaünUniversity of Grenoble Alpes
Formalise-2019-papers10:05 - 10:30
Full-paper