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

Formal Verification of UML Models Based on TLA

作　　者：梁盟磊[1] 王小平[1] 薛小平[2] 李刚[2] 

机构地区：[1]同济大学电子与信息工程学院计算机科学与技术系,上海200092 [2]同济大学电子与信息工程学院信息与通信工程系,上海200092

出　　处：《计算机工程》2011年第2期72-74,共3页Computer Engineering

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

摘　　要：统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题,从UML模型的静态结构和动态行为2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。UML can not carry out a formal check directly to models established. In order to solve the problem, based on the static structures and dynamic behaviors of UML models, this paper proposes two kinds of methods combing Temporal Logic of Actions（TLA） for model formalization. Formal description method for translating the UML model to TLA＋ is given, and TLC toolkit is used to verify TLA＋ specification. An example of UML model translation and verification is given to show the effectiveness of the method.

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

分 类 号：TP391[自动化与计算机技术—计算机应用技术]