QQ客服 官方微博 反馈留言

	Research of model checking UML
	Zhang Pin ; Luo Gui-ming
	2010-05-07 ; 2010-05-07
关键词	Practical/ automata theory software engineering software reliability Unified Modeling Language/ model checking UML Unified Modeling Language software system design software system analysis system reliability simple PROMELA interpreter model-checker formal method statecharts diagram/ C6140D High level languages C6110F Formal methods C6110B Software engineering techniques
中文摘要	Unified Modeling Language (UML) is the most commonly used method in software system design and analysis, and how to verify that the UML model satisfies some properties is a very important issue. Model Checking is an efficient automatic technique for the improvement of system's reliability, and this paper is a research into how to check UML model through the Simple PROMELA Interpreter (SPIN) model-checker. After describing the UML model using formal method, we first used hierarchical automata to express statecharts diagram. In addition, we translated the statechars and part of the class diagram into PROMELA based on the operational semantic of hierarchical automata, and verified the model by using Simple PROMELA Interpreter ( SPIN) to test if it satisfied the LTL properties. We also verified the consistency between sequence diagram and statecharts diagram by using LTL formula to express sequence diagram. Finally, based on the method, we developed a model checker tool called UMLChecker.
语种	中文 ; 中文
出版者	Science Press ; China
内容类型	期刊论文
源URL	[http://hdl.handle.net/123456789/16758]
专题	清华大学
推荐引用方式 GB/T 7714	Zhang Pin,Luo Gui-ming. Research of model checking UML[J],2010, 2010.
APA	Zhang Pin,&Luo Gui-ming.(2010).Research of model checking UML..
MLA	Zhang Pin,et al."Research of model checking UML".(2010).

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。