TY - GEN
T1 - Timed automata with disjoint activity
AU - Muñiz, Marco
AU - Westphal, Bernd
AU - Podelski, Andreas
PY - 2012/10/1
Y1 - 2012/10/1
N2 - The behavior of timed automata consists of idleness and activity, i.e. delay and action transitions. We study a class of timed automata with periodic phases of activity. We show that, if the phases of activity of timed automata in a network are disjoint, then location reachability for the network can be decided using a concatenation of timed automata. This reduces the complexity of verification in Uppaal-like tools from quadratic to linear time (in the number of components) while traversing the same reachable state space. We provide templates which imply, by construction, the applicability of sequential composition, a variant of concatenation, which reflects relevant reachability properties while removing an exponential number of states. Our approach covers the class of TDMA-based (Time Division Multiple Access) protocols, e.g. FlexRay and TTP. We have successfully applied our approach to an industrial TDMA-based protocol of a wireless fire alarm system with more than 100 sensors.
AB - The behavior of timed automata consists of idleness and activity, i.e. delay and action transitions. We study a class of timed automata with periodic phases of activity. We show that, if the phases of activity of timed automata in a network are disjoint, then location reachability for the network can be decided using a concatenation of timed automata. This reduces the complexity of verification in Uppaal-like tools from quadratic to linear time (in the number of components) while traversing the same reachable state space. We provide templates which imply, by construction, the applicability of sequential composition, a variant of concatenation, which reflects relevant reachability properties while removing an exponential number of states. Our approach covers the class of TDMA-based (Time Division Multiple Access) protocols, e.g. FlexRay and TTP. We have successfully applied our approach to an industrial TDMA-based protocol of a wireless fire alarm system with more than 100 sensors.
UR - http://www.scopus.com/inward/record.url?scp=84866697018&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-33365-1_14
DO - 10.1007/978-3-642-33365-1_14
M3 - Article in proceeding
AN - SCOPUS:84866697018
SN - 9783642333644
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 188
EP - 203
BT - Formal Modeling and Analysis of Timed Systems - 10th International Conference, FORMATS 2012, Proceedings
T2 - 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012
Y2 - 18 September 2012 through 20 September 2012
ER -