主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
夏薇,姚益平,慕晓冬.面向事件图和事件时态逻辑的模型检验方法.软件学报,2013,24(3):421-432
面向事件图和事件时态逻辑的模型检验方法
Model Checking for Event Graphs and Event Temporal Logic
投稿时间:2011-06-23  修订日期:2011-11-17
DOI:10.3724/SP.J.1001.2013.04162
中文关键词:  事件图  事件时态逻辑  模型检验  Büchi自动机  转换
英文关键词:event graph  event temporal logic  model checking  Büchi automaton  transformation
基金项目:国家自然科学基金(61170048); 国家教育部博士点基金(200899980004)
作者单位E-mail
夏薇 国防科学技术大学 计算机学院,湖南 长沙 410073
第二炮兵工程大学 计算机系,陕西 西安 710025 
weiwei32329@163.com 
姚益平 国防科学技术大学 计算机学院,湖南 长沙 410073  
慕晓冬 第二炮兵工程大学 计算机系,陕西 西安 710025  
摘要点击次数: 3195
全文下载次数: 3434
中文摘要:
      针对目前没有适合直接对事件图模型进行性质规约的时态逻辑语言,提出一种基于事件的时态逻辑(event temporal logic,简称ETL).ETL以事件作为原子命题,根据事件图的特点增加了对事件取消操作、模型实例化、时间约束和同时事件优先级的表达能力,便于仿真领域的用户在模型检验过程中简洁地对基于事件图的模型应满足的性质进行描述.然后,在ETL公式和自动机理论的基础上,给出了面向事件图和ETL的模型检验方法来判断事件图模型是否满足ETL描述的性质规约.实例验证了ETL对事件图模型具有足够的表达能力以及该方法的有效性.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利