基于TLA的UML模型形式化验证

摘要：

统一建模语言(UML)不能直接对所建直模型的正确性进行形式化验证.为解决上述问题,从UML模型的静态结构和动态行为2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性.通过实例分析证明了该方法的有效性.

关键词：形式化方法、形式化验证、统一建模语言、行为时序逻辑

所属期刊栏目：37

分类号：TP391(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目60972036

在线出版日期：2011-04-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：72-74