面向事件图和事件时态逻辑的模型检验方法

作     者：夏薇 姚益平 慕晓冬 

作者机构：国防科学技术大学计算机学院湖南长沙410073 第二炮兵工程大学计算机系陕西西安710025 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2013年第24卷第3期

页      面：421-432页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金(61170048) 国家教育部博士点基金(200899980004) 

主　　题：事件图 事件时态逻辑 模型检验 Büchi自动机 转换 

摘      要：针对目前没有适合直接对事件图模型进行性质规约的时态逻辑语言,提出一种基于事件的时态逻辑(event temporal logic,简称ETL).ETL以事件作为原子命题,根据事件图的特点增加了对事件取消操作、模型实例化、时间约束和同时事件优先级的表达能力,便于仿真领域的用户在模型检验过程中简洁地对基于事件图的模型应满足的性质进行描述.然后,在ETL公式和自动机理论的基础上,给出了面向事件图和ETL的模型检验方法来判断事件图模型是否满足ETL描述的性质规约.实例验证了ETL对事件图模型具有足够的表达能力以及该方法的有效性.