原文服务方: 计算机应用研究       
摘要:
针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of action,TLA)的事件图模型形式化验证方法.该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型检验工具进行验证.这种方法不仅能够有效提高仿真模型的正确性,而且能够提高模型的可重用性,简化仿真模型建模与验证过程.最后利用TLA模型检验工具对实例进行了验证,实验结果表明了该方法的有效性.
推荐文章
基于活性顺序图的形式化验证方法及工具研究
活性顺序图
形式化验证
软件开发过程
基于Rebeca模型的硬件设计形式化验证
形式化验证
Rebeca模型
Modere
基于TLA的UML模型形式化验证
形式化方法
形式化验证
统一建模语言
行为时序逻辑
基于符号模型检测的符号有向图故障诊断解形式化验证
SDG模型
符号模型检测
动态验证信息
动态验证策略
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 基于TLA的事件图模型形式化验证方法
来源期刊 计算机应用研究 学科
关键词 仿真模型 验证、确认和认定 模型检验 行为时态逻辑 事件图
年,卷(期) 2011,(11) 所属期刊栏目 软件技术研究
研究方向 页码范围 4171-4173,4187
页数 分类号 TP391
字数 语种 中文
DOI 10.3969/j.issn.1001-3695.2011.11.045
五维指标
作者信息
序号 姓名 单位 发文数 被引次数 H指数 G指数
1 姚益平 国防科学技术大学计算机学院 27 290 10.0 16.0
2 夏薇 国防科学技术大学计算机学院 8 36 4.0 5.0
4 慕晓冬 第二炮兵工程学院计算机系 64 234 8.0 9.0
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (5)
共引文献  (7)
参考文献  (5)
节点文献
引证文献  (6)
同被引文献  (13)
二级引证文献  (8)
1994(1)
  • 参考文献(0)
  • 二级参考文献(1)
2001(2)
  • 参考文献(0)
  • 二级参考文献(2)
2002(1)
  • 参考文献(0)
  • 二级参考文献(1)
2005(1)
  • 参考文献(1)
  • 二级参考文献(0)
2008(1)
  • 参考文献(1)
  • 二级参考文献(0)
2009(3)
  • 参考文献(2)
  • 二级参考文献(1)
2011(1)
  • 参考文献(1)
  • 二级参考文献(0)
2011(1)
  • 参考文献(1)
  • 二级参考文献(0)
  • 引证文献(0)
  • 二级引证文献(0)
2013(4)
  • 引证文献(4)
  • 二级引证文献(0)
2014(2)
  • 引证文献(2)
  • 二级引证文献(0)
2015(1)
  • 引证文献(0)
  • 二级引证文献(1)
2016(3)
  • 引证文献(0)
  • 二级引证文献(3)
2017(2)
  • 引证文献(0)
  • 二级引证文献(2)
2019(2)
  • 引证文献(0)
  • 二级引证文献(2)
研究主题发展历程
节点文献
仿真模型
验证、确认和认定
模型检验
行为时态逻辑
事件图
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
计算机应用研究
月刊
1001-3695
51-1196/TP
大16开
1984-01-01
chi
出版文献量(篇)
21004
总下载数(次)
0
论文1v1指导