期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于TLA的UML模型形式化验证 被引量：3

Formal Verification of UML Models Based on TLA
下载PDF
导出
摘要 统一建模语言(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.
作者 梁盟磊 王小平 薛小平 李刚
机构地区 同济大学电子与信息工程学院计算机科学与技术系 同济大学电子与信息工程学院信息与通信工程系
出处 《计算机工程》 CAS CSCD 北大核心 2011年第2期72-74,共3页 Computer Engineering
基金 国家自然科学基金资助项目(60972036)
关键词 形式化方法 形式化验证 统一建模语言 行为时序逻辑 formal method formal verification UML Temporal Logic of Actions（TLA）
分类号 TP391 [自动化与计算机技术—计算机应用技术]
  • 相关文献

参考文献5

  • 1陈振庆.基于SHOIN(D)的UML类图形式化方法[J].计算机工程,2009,35(19):43-45. 被引量：16
  • 2Merz S. The Specification Language TLA+[M]//Bjomer D, Henson M C. Logics of Specification Languages: Part 11. Berlin, Germany: Springer, 2008:401-451.
  • 3Booch G, Rumbaugh J, Jacobson I. The Unified Modeling Language User Guide[M]. 2nd ed. Beijing, China: Machine Press, 2006.
  • 4FreinkeI L. An Approach to Combining UML and TLA+ in Software Speciation[D]. Reno: University of Nevada, 2003.
  • 5Shrotri U, Bhaduri P, Venkatesh R. Model Checking Visual Specification of Requirements [C]//Proc. of International Conference on Software Engineering and Formal Methods. Brisbane, Australia: [s. n.], 2003.

二级参考文献6

共引文献15

同被引文献24

  • 1曾红卫,滕中梅.用Z形式化描述的软件设计模式[J].计算机工程,2006,32(13):69-70. 被引量：3
  • 2CLARKE E M, EMERSON E A, SIFAKIS J. Model checking: algorithmic verification and debugging [ J ]. Communications of the ACM,2009,52 ( 11 ) :75- 84.
  • 3LAMPORT L. Specifying systems : the TLA + language and tools for hardware and software engineers [ M ]. Boston: Addison-Weslet,2002.
  • 4SAVAGE E L, SCHRUBEN L W, YUCESAN E. On the generality of event-graph models[ J]. INFORMS Journal on Computing, 2005, 17(1):3-9.
  • 5FUJIMOTO R M. Parallel and distributed simulation systems [ M ]. New York : Wiley-Interscience Publication, 2002.
  • 6Dietrich J,Elgar C.A Formal Description of Design Patterns Using OWL[C]//Proceedings of 2005 Australian Conference on Software Engineering.Washington D.C.,USA:IEEE Computer Society,2005:243-250.
  • 7Kim S K,Carrington D.A Formalism to Describe Design Patterns Based on Role Concepts[J].Formal Aspects of Computing,2009,21(5):397-420.
  • 8袁崇义.Petri网原理[M].北京:科学出版社,2013.
  • 9Girault C,Valk R.Petri Nets for Systems Engineering:A Guide to Modeling,Verification,and Applications[M].Berlin,Germany:Springer-Verlag,2003.
  • 10Gamma E,Helm R,Johnson R,et al.Design Pattern:Elements of Reusable Object-oriented Software[M].Boston,USA:Addison-Wesley,1995.

引证文献3

二级引证文献8

计算机工程
2011年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部