Title :
Emerald: An Automated Modeling and Verification Tool for Component-Based Real-Time Systems
Author :
Zhang, Yizhou ; Lin, Hao ; Li, Guoqiang
Author_Institution :
Sch. of Software, Shanghai Jiao Tong Univ., Shanghai, China
Abstract :
Controller automata, extending timed automata, are a formal theory to model and analyze real-time systems with mutex components. Given a strict partial order over states, an ordered controller automaton can be faithfully translated into a timed automaton. We present a tool named Emerald to translate ordered controller automata into timed automata and perform the transformation between their specifications in order to use the existing model checking engine, UPPAAL.
Keywords :
automata theory; formal verification; real-time systems; Emerald; automated modeling; component-based real-time systems; controller automata; mutex components; timed automata; verification tool; Automata; Clocks; Computational modeling; Engines; Real-time systems; Software; Real-time systems; controller automata; modeling; verification;
Conference_Titel :
Quality Software (QSIC), 2012 12th International Conference on
Conference_Location :
Xi´an, Shaanxi
Print_ISBN :
978-1-4673-2857-9
DOI :
10.1109/QSIC.2012.27
