文献类型：期刊文章

作　　者：夏薇[1,2] 姚益平[1] 慕晓冬[2]

机构地区：[1]国防科学技术大学计算机学院,长沙410073 [2]第二炮兵工程学院计算机系,西安710025

出　　处：《计算机应用研究》

基　　金：国家自然科学基金资助项目(60773019);国家博士点基金资助项目(200899980004)

年　　份：2011

卷　　号：28

期　　号：11

起止页码：4171-4173

语　　种：中文

收录情况：AJ、BDHX、BDHX2008、CSA-PROQEUST、CSCD、CSCD2011_2012、IC、INSPEC、JST、RCCSE、UPD、ZGKJHX、ZMATH、核心刊

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

关 键 词：仿真模型 验证、确认和认定  模型检验  行为时态逻辑  事件图

分 类 号：TP391]