面向事件图和事件时态逻辑的模型检验方法
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

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


Model Checking for Event Graphs and Event Temporal Logic
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    This paper proposes an event temporal logic (ETL) because there has been no suitable temporal logic that can directly describe the properties of event graph (EG) models. ETL takes events as its atomic propositions and has the abilities to describe the event canceling edge, the passing parameter values between events, time constraints and the priorities of coinstantaneous events, which can facilitate the description of properties for EGs. A model checking method for EG and ETL on the basis of theory of automata is also proposed in this paper to check whether properties hold for models, according to the accepted language is an empty set or not. The experimental results show ETL is powerful enough to describe EG models, and the model checking method for EG and ETL is effective.

    参考文献
    相似文献
    引证文献
引用本文

夏薇,姚益平,慕晓冬.面向事件图和事件时态逻辑的模型检验方法.软件学报,2013,24(3):421-432

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2011-06-23
  • 最后修改日期:2011-11-17
  • 录用日期:
  • 在线发布日期: 2013-03-01
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号