期刊文献+
共找到1篇文章
< 1 >
每页显示 20 50 100
基于TLA的事件图模型形式化验证方法 被引量:4
1
作者 夏薇 姚益平 慕晓冬 《计算机应用研究》 CSCD 北大核心 2011年第11期4171-4173,4187,共4页
针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logicof action,TLA)的事件图模型形式化验证方法。该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模... 针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logicof action,TLA)的事件图模型形式化验证方法。该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型检验工具进行验证。这种方法不仅能够有效提高仿真模型的正确性,而且能够提高模型的可重用性,简化仿真模型建模与验证过程。最后利用TLA模型检验工具对实例进行了验证,实验结果表明了该方法的有效性。 展开更多
关键词 仿真模型 验证、确认和认定 模型检验 行为时态逻辑 事件图
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部