model checking linear duration invariants of networks of automata

	model checking linear duration invariants of networks of automata
	Zhang Miaomiao; Liu Zhiming; Zhan Naijun
	2010
会议名称	3rd IPM International Conference on Fundamentals of Software Engineering, Conference, FSEN 2009
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	244-259
会议日期	April 15,
会议地点	Kish Island, Iran
收录类别	EI
出版地	Germany
ISSN	3029743
ISBN	3642116221
部门归属	(1) School of Software Engineering, Tongji University, Shanghai, China; (2) International Institute of Software Technology, United Nations University, China; (3) Lab. of Computer Science, Institute of Software, CAS, Beijing, China
摘要	Linear duration invariants (LDIs) are important safety properties of real-time systems. In this paper, we reduce the problem of verification of a network of timed automata against an LDI to an equivalent problem of model checking whether a failure state is never reached. Our approach is first to transform each component automaton Ai of the network A to an automaton Gi. The transformation helps us to record entry and exit to critical locations that appear in the LDI. We then introduce an auxiliary checker automaton S and define a failure state to verify the LDI on a given interval. Since a model checker checks exhaustively, a failure of the checker automaton to find the failure state will prove that the LDI holds. © 2010 Springer.
关键词	Computer Software Model Checking Permanent Magnets Real Time Systems Robots Safety Engineering Translation (Languages)
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/8830
专题	基础软件与系统重点实验室
推荐引用方式 GB/T 7714	Zhang Miaomiao,Liu Zhiming,Zhan Naijun. model checking linear duration invariants of networks of automata[C]. Germany,2010:244-259.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
model checking linea（318KB）			开放获取	--	请求全文