axiomatic temporal logic programs verification

	axiomatic temporal logic programs verification
	Yang Xiaoxiao ; Duan Zhenhua
	2010
会议名称	2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010
会议日期	August 25,
会议地点	Taipei, Taiwan
关键词	Computer simulation languages Logic programming Safety engineering Software engineering
页码	87-94
英文摘要	In this paper, we investigate the axiomatic system of Modeling Simulation and Verification Language (MSVL). To this end, a set of state axioms and state inference rules is given. They are useful to deduce a program into its normal form. Further, a propositional projection temporal logic is used as assertion language to describe the required property of a program. Moreover, to deduce a program over an interval, a set of rules in terms of triple like Hoare logic is formalized. These rules enable us to deduce a program in its normal form at the current state to the next one and to verify safety, liveness properties over an interval. © 2010 IEEE.
收录类别	EI
会议主办者	National Taiwan University; Res. Cent. Inf. Technol. Innov., Acad. Sin.; National Science Council; Ministry of Education; IEEE Computer Society
会议录	Proceedings - 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010
会议录出版地	United States
ISBN号	9780770000000
内容类型	会议论文
源URL	[http://124.16.136.157/handle/311060/8682]
专题	软件研究所_计算机科学国家重点实验室 _会议论文
推荐引用方式 GB/T 7714	Yang Xiaoxiao,Duan Zhenhua. axiomatic temporal logic programs verification[C]. 见:2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010. Taipei, Taiwan. August 25,.