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

基于自动机理论的UML活动图模型检验方法 被引量：1

Automaton Theory-based Model Checking Method for UML Activity Diagram
下载PDF
导出
摘要 UML活动图被认为是最合适的软件过程描述语言,研究UML活动图的模型检验方法是很有必要的。提出一种基于自动机理论的UML活动图的模型检验方法。该方法给出UML活动图的形式语义,通过计算RTC-STEP,得到LTS,并将LTS映射到Büchi自动机,用LTL表示系统性质,并将LTL公式转换为相应的Büchi自动机,用基于自动机理论的模型检验方法检验UML活动图。 UML activity diagram is regarded as the most suitable language to describing the software process. It is worth to researching the approach of model checking UML activity diagram. An approach of model checking UML activity diagram was provided. The formal semantics of UML activity diagram was given. LTS （Labeled Transition System） was deduced by computing the RTC-STEP. And then the LTS could be mapped to a Bǖchi automaton. The system properties could be described by LTL. LTL formula could be translated to a Bǖchi automaton. UML activity diagram could be checked by automaton theory-based model checking method.
作者 王聪 王智学
机构地区 解放军理工大学通信工程学院 解放军理工大学指挥自动化学院
出处 《系统仿真学报》 EI CAS CSCD 北大核心 2007年第22期5311-5314,共4页 Journal of System Simulation
基金 总装备部十五预研项目(413060103)
关键词 UML活动图 形式语义 模型检验 BÜCHI自动机 UML activity diagram formal semantics model checking Bǖchi automaton
分类号 TP311.5 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献13

  • 1OMG. OMG unified modeling language specification (Version 1.5)[R]. Needham: Object Management Group, Inc., 2003.
  • 2Rumbaugh J, Jacobson I, Booch G. The Unified Modeling language Reference Manual [M]. Boston: Addison-Wesley, 1999.
  • 3Mikk E, Lakhnech Y, Siegel M, et al. Implementing Statecharts in PROMELA/SPIN [C]// Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT'98). Washington, DC: IEEE Computer Society, 1998.
  • 4Lilius J, Paltor IP. vUML: a tool for verifying UML models [C]//Hall R, Tyugu E, eds. Proceedings of the 14th IEEE International Conference on Automated Software Engineering. Washington, DC: IEEE Computer Society, 1999: 255-258.
  • 5Gnesi S, Latella D. Model checking UML statecharts diagrams using JACK [C]// Proceedings of the 4th IEEE International Symposium on High-Assurance Systems Engineering. Washington, DC: IEEE Computer Society, 1999: 46-55.
  • 6Eshuis R, Wieringa R. A formal semantics for UML activity diagrams [R]. Technical Report TR-CTIT-01-04. Hengelo, Netherlands: University of Tweme, 2001.
  • 7Gerth R, Peled D, Vardi MY, et al. Simple on-the-fly automatic verification of linear temporal logic [C]//Dembinski P, Sredniawa M, eds. Proceedings of the 15th International Symposium on Protocol Specification Testing and Verification. Boston: Kluwer Academic Publishers. 1995: 3-18.
  • 8Daniele M, Giunchiglia F, Vardi M. Improved automata generation for linear temporal logic [C]//N Halbwachs, D Peled, editors, Proc. of Computer Aided Verication: 11th Int. Conf., CAV'99, Trento, Italy: LNCS 1633. 1999: 249-260.
  • 9Somenzi F, Bloem R. Efficient Buechi automata from LTL Formulae [C]//Proc. Of the 12th International conference on Computer Aided Verification (CAV 2000). Chicago, USA: Springer, LNCS 1855. 2000: 247-263.
  • 10Gastin P, Oddoux D. Fast LTL to Buechi Automata Translation[C]// Proc. of the 13th International Conference on Computer Aided Verification (CAV 2001), Pads, France: Springer, LNCS 2102. July 2001: 53-65.

同被引文献12

  • 1Hermanns H,Kwiatkowska M,Norman G,et al.On the Use of MTBDDs for Performability Analysis and Veri?cation of Stochastic Systems[J].Journal of Logic and Algebraic Programming,2003,56(1/2):23-67.
  • 2Donaldson A F,Miller A.Symmetry Reduction for Pro-babilistic Model Checking Using Generic Representatives[C]// Proc.of the 4th International Conference on Automated Technology for Verification and Analysis.[S.l.]:Springer-Verlag,2006:9-23.
  • 3Kwiatkowska M,Norman G,Parker D.Symmetry Reduction for Probabilistic Model Checking[C]//Proc.of the 18th International Conference on Computer Aided Verification.Seattle,USA:Springer-Verlag,2006:7-20.
  • 4Pekergin N,Younes S.Stochastic Model Checking with Stochastic Comparison[C]//Proc.of European Performance Engineering Workshop.Berlin,Germany:Springer-Verlag,2005:109-123.
  • 5Zhang Lijun,Jansen D N,Nielson F,et al.Automata-based CSL Model Checking[C]//Proc.of the 38th International Colloquium on Automaton,Languages and Programming.Berlin,Germany:Springer-Verlag,2011:271-282.
  • 6Desharnais J,Gupta V,Jagadeesan R,et al.Weak Bisi-mulation is Sound and Complete for PCTL*[J].Information and Computation,2010,208(2):203-219.
  • 7雷丽晖,段振华.一种基于扩展有限自动机验证组合Web服务的方法[J].软件学报,2007,18(12):2980-2990. 被引量：37
  • 8钮俊,曾国荪,王伟.基于模型检测的时间空间性能验证方法[J].计算机学报,2010,33(9):1621-1633. 被引量：6
  • 9聂锡宁,蔡国永.Petri网的重写逻辑模型及其属性验证[J].桂林电子科技大学学报,2011,31(3):208-212. 被引量：1
  • 10李力行,金芝,李戈.基于时间自动机的物联网服务建模和验证[J].计算机学报,2011,34(8):1365-1377. 被引量：48

引证文献1

系统仿真学报
2007年 第22期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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