摘要
针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logicof action,TLA)的事件图模型形式化验证方法。该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型检验工具进行验证。这种方法不仅能够有效提高仿真模型的正确性,而且能够提高模型的可重用性,简化仿真模型建模与验证过程。最后利用TLA模型检验工具对实例进行了验证,实验结果表明了该方法的有效性。
This paper presented a formal verification method for event graph models based on TLA,because there was no existing formal method.This method defined event graph model and its properties in TLA language,utilizing the characteristic of TLA which could describe models and properties in a single language and its similarity to event graphs.So the model could be verified by TLA model checker.This method not only effectively improved the correctness and reusability of simulation models,but also facilitated the process for modeling and verification of simulation models.A case study was verified by TLA based model checker,and the experimental results show the effectiveness of this method.
出处
《计算机应用研究》
CSCD
北大核心
2011年第11期4171-4173,4187,共4页
Application Research of Computers
基金
国家自然科学基金资助项目(60773019)
国家博士点基金资助项目(200899980004)
关键词
仿真模型
验证、确认和认定
模型检验
行为时态逻辑
事件图
simulation models
verification
validation ＆ accreditation（VV＆A）
model checking
temporal logic of action（TLA）
event graph
