Temporal Logics and Model Checking Algorithms for ZIAs

摘要：

In this paper, we first propose a specification ap-proach combining interface automata and Z language. This approach can be used to describe temporal properties and data properties of software components. A branching time logic for ZIAs is presented. We then give an algorithm for model checking this logic on ZIAs with finite domain. Furthermore, we present a mu-calculus logic for ZIAs, and give a model checking algorithm for this logic.

关键词： model checking interface automata Z notation temporal logic

作者: Zining Ca0

作者单位: National Key Laboratory of Science and Technology on Avionics System Integration Shanghai 200233. P. R. China;Department of Computer Science and Technology Nanjing University of Aero. & Astro.Nanjing 210016, P. R. China;Provincial Key Laboratory for Computer Information Processing Technology, Soochow University Suzhou 215006. P. R. China

会议类型: 国际会议

会议名称: The 2nd International Conference on Software Engineering and Data Mining(IEEE 第二届国际软件工程和数据挖掘学术大会 SEDM 2010)

会议地点: 成都

会议语种:英文

页码: 527-532

在线出版日期: 2010-06-23（万方平台首次上网日期，不代表论文的发表时间）