摘要： 统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题，从UML模型的静态结构和动态行为 2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法，在此基础上提出将UML模型转化为TLA+的形式化描述方法，并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。
关键词:
形式化方法,
形式化验证,
统一建模语言,
行为时序逻辑
Abstract: 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.
Key words:
formal method,
formal verification,
UML,
Temporal Logic of Actions(TLA)
中图分类号:
梁盟磊, 王小平, 薛小平, 李刚. 基于TLA的UML模型形式化验证[J]. 计算机工程, 2011, 37(2): 72-74.
LIANG Meng-Lei, WANG Xiao-Beng, XUE Xiao-Beng, LI Gang. Formal Verification of UML Models Based on TLA[J]. Computer Engineering, 2011, 37(2): 72-74.