基于TLA的事件图模型形式化验证方法

• 作者: 夏薇 姚益平 慕晓冬
• 来源期刊: 计算机应用研究
• 关键词: 仿真模型 验证、确认和认定 模型检验 行为时态逻辑 事件图
• 年，卷（期）: 2011,（11）
• 所属期刊栏目: 软件技术研究
• 页码范围: 4171-4173,4187
• 分类号: TP391
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2011.11.045

摘要

针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of action,TLA)的事件图模型形式化验证方法.该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型检验工具进行验证.这种方法不仅能够有效提高仿真模型的正确性,而且能够提高模型的可重用性,简化仿真模型建模与验证过程.最后利用TLA模型检验工具对实例进行了验证,实验结果表明了该方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	姚益平	国防科学技术大学计算机学院	27	290	10.0	16.0
2	夏薇	国防科学技术大学计算机学院	8	36	4.0	5.0
4	慕晓冬	第二炮兵工程学院计算机系	64	234	8.0	9.0