emerald: an automated modeling and verification tool for component-based real-time systems

ISCAS OpenIR

	emerald: an automated modeling and verification tool for component-based real-time systems
	Zhang Yizhou; Lin Hao; Li Guoqiang
	2012
会议名称	12th International Conference on Quality Software, QSIC 2012
会议录名称	Proceedings - International Conference on Quality Software
页码	120-123
会议日期	August 27, 2012 - August 29, 2012
会议地点	Xi'an, Shaanxi, China
收录类别	EI
ISSN	1550-6002
ISBN	9780769548333
部门归属	(1) BASICS School of Software Shanghai Jiao Tong University China; (2) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences China
摘要	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. © 2012 IEEE.; 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. © 2012 IEEE.
关键词	Model Checking Models Real Time Systems Verification
主办者	Northwest Polytechnic University; The University of Hong Kong; University of L'Aquila
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15862
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Zhang Yizhou,Lin Hao,Li Guoqiang. emerald: an automated modeling and verification tool for component-based real-time systems[C],2012:120-123.