Abstract | ||
---|---|---|
Timed automata are popular for formally analyzing real-time systems. However, it is difficult to depict real-time systems with compositional components that interact with each other in a synchronization way or a mutex way. Synchronized components are modeled using parallel composition of timed automata by Larsen et al. This paper proposes controller automata to represent real-time systems with mutex components. In a controller automaton each state corresponds to a timed automaton with a built-in mechanism of relations, e.g., preemptions, in which every such timed automaton models a component of the real-time system. It is shown that given a strict partial order over states, an ordered controller automaton can be translated into a timed automaton. Various analyses are thus performed by checking the reachability to an error state. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1109/IPDPSW.2010.5470825 | Int. J. Found. Comput. Sci. |
Keywords | DocType | Volume |
automata theory,timed automata,compositional component,mutex,mutex component,real-time system,timed automaton model,formal analysis,controller automata,real-time systems,real time systems | Conference | 23 |
Issue | ISBN | Citations |
4 | 978-1-4244-6533-0 | 2 |
PageRank | References | Authors |
0.39 | 23 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Guoqiang Li | 1 | 85 | 28.36 |
Xiaojuan Cai | 2 | 36 | 5.95 |
Shoji Yuen | 3 | 178 | 18.38 |