基于TLA的事件图模型形式化验证方法OA北大核心CSCDCSTPCD
Formal verification of event graph models based on TLA
针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of 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 reusa…查看全部>>
夏薇;姚益平;慕晓冬
国防科学技术大学计算机学院,长沙410073第二炮兵工程学院计算机系,西安710025国防科学技术大学计算机学院,长沙410073
信息技术与安全科学
仿真模型验证、确认和认定模型检验行为时态逻辑事件图
simulation models verification, validation & accreditation( VV&A) model checking temporal logic of action (TLA) event graph
《计算机应用研究》 2011 (11)
基于Agent的并行仿真支撑技术研究
4171-4173,4187,4
国家自然科学基金资助项目(60773019)国家博士点基金资助项目(200899980004)
评论