|
|||||
|
|
| 基于TLA的事件图模型形式化验证方法* | |
| 引用本文： | 夏薇,姚益平,慕晓冬.基于TLA的事件图模型形式化验证方法*[J].计算机应用研究,2011,28(11):4171-4173. |
| 作者姓名： | 夏薇 姚益平 慕晓冬 |
| 作者单位： | 1. 国防科学技术大学计算机学院,长沙410073;第二炮兵工程学院计算机系,西安710025 2. 国防科学技术大学计算机学院,长沙,410073 3. 第二炮兵工程学院计算机系,西安,710025 |
| 基金项目： | 国家自然科学基金资助项目（60773019）；国家博士点基金资助项目（200899980004） |
| 摘 要： | 针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of action,TLA)的事件图模型形式化验证方法.该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型... |
| 关 键 词： | 仿真模型 验证、确认和认定 模型检验 行为时态逻辑 事件图 |
Formal verification of event graph models based on TLA |
|
| XIA Wei,YAO Yi-ping,MU Xiao-dong.Formal verification of event graph models based on TLA[J].Application Research of Computers,2011,28(11):4171-4173. | |
| Authors: | XIA Wei YAO Yi-ping MU Xiao-dong |
| Affiliation: | XIA Wei1,2,YAO Yi-ping1,MU Xiao-dong2 (1.School of Computer,National University of Defense Technology,Changsha 410073,China,2.Dept.of Computer Science,Xi'an Hi-Tech Institute,Xi'an 710025,China) |
| Abstract: | 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. |
| Keywords: | simulation models verification validation & accreditation(VV&A) model checking temporal logic of action(TLA) event graph |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《计算机应用研究》浏览原始摘要信息 | |
| 点击此处可从《计算机应用研究》下载全文 | |