作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2011, Vol. 37 ›› Issue (2): 72-74. doi: 10.3969/j.issn.1000-3428.2011.02.025

• 软件技术与数据库 • 上一篇    下一篇

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

梁盟磊a,王小平a,薛小平b,李 刚b   

  1. (同济大学电子与信息工程学院 a. 计算机科学与技术系;b. 信息与通信工程系,上海 200092)
  • 出版日期:2011-01-20 发布日期:2011-01-25
  • 作者简介:梁盟磊(1985-),男,硕士研究生,主研方向
  • 基金资助:
    国家自然科学基金资助项目(60972036)

Formal Verification of UML Models Based on TLA

LIANG Meng-lei a, WANG Xiao-ping a, XUE Xiao-ping b, LI Gang b   

  1. (a. Department of Computer Science and Technology; b. Department of Information and Communication Engineering,College of Electronics and Information, Tongji University, Shanghai 200092, China)
  • Online:2011-01-20 Published:2011-01-25

摘要: 统一建模语言(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)

中图分类号: