loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
19th IEEE International Parallel and Distributed Processing Symposium (IPDPS'05) - Workshop 2
Compatibility Between Shared Variable Valuations in Timed Automaton Network Model-Checking
Denver, Colorado
April 04-April 08
ISBN: 0-7695-2312-9
Zhao Jianhua, Nanjing University, Jiangsu, P.R. China
Zhou Xiuyi, Nanjing University, Jiangsu, P.R. China
Li Xuandong, Nanjing University, Jiangsu, P.R. China
Zheng Guoliang, Nanjing University, Jiangsu, P.R. China
Many real-time systems are modelled as timed automaton networks, which are parallel compositions of timed automata. Those timed automata interact with each other through shared variables and/or communication channels. In the literate, symbolic states with different shared variable valuations are treated as distinct ones. This paper presents a compatibility relation between shared variable valuations. Using this relation, the reachability analysis algorithm can avoid exploring all the states with different shared variable valuations.
An algorithm is presented in this paper to detect compatible shared variable valuations. A compact data structure is also proposed to record the shared variable valuation sets found by this algorithm. Based on these results, an optimized reachability analysis algorithm is presented. Case studies show that our technique improves the space-efficiency of reachability analysis significantly.
Index Terms:
model checking, timed automaton, formal method
Citation:
Zhao Jianhua, Zhou Xiuyi, Li Xuandong, Zheng Guoliang, "Compatibility Between Shared Variable Valuations in Timed Automaton Network Model-Checking," ipdps, vol. 3, pp.129a, 19th IEEE International Parallel and Distributed Processing Symposium (IPDPS'05) - Workshop 2, 2005
Usage of this product signifies your acceptance of the Terms of Use.