中文摘要：

针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑（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.