| 基于Spin的UML状态图模型检查的设计与实现 |
| |
| 引用本文： | 郭伟,缪力,张大方,闵应骅.基于Spin的UML状态图模型检查的设计与实现[J].计算机工程与应用,2008,44(10):43-47. |
| |
| 作者姓名： | 郭伟 缪力 张大方 闵应骅 |
| |
| 作者单位： | 1.湖南大学 软件学院，长沙 410082 2.湖南大学 计算机与通信学院，长沙 410082 3.中国科学院 计算技术研究所，北京 100080 |
| |
| 基金项目： | 国家部委基础科研“十一五”项目，国家自然科学基金(the National Natural Science Foundation of China under Grant No.60673155) |
| |
| 摘 要： | UML已经是软件建模方面的标准语言，UML Statechart描述了系统在其生命周期中的动态行为。随着系统规模的扩大和复杂度的提高，Statechart往往包含设计者所未预料到的隐患，通过模型检查来对Statechart进行穷举检验就成为一个重要课题，首先给出了含层次、并发Statechart的语义；随后提出了对Statechart进行模型检查的一种新方法，并且已经编写软件SC2Spin实现此方法，该方法使用了提出的Statechart山脉算法和迁移提取法，可以将一个Statechart自动转化为Spin的输入语言Promela，从而验证Statechart的死锁、活锁等错误和时序逻辑公式。
|
| 关 键 词： | 模型检查 Statechart Statechart山脉算法 迁移提取 Spin |
| 文章编号： | 1002-8331(2008)10-0043-05 |
| 收稿时间： | 2007-7-20 |
| 修稿时间： | 2007年7月20日 |
Model checking UML Statechart based on Spin |
| |
| GUO Wei,MIAO Li,ZHANG Dafang,MIN Yinghua.Model checking UML Statechart based on Spin[J].Computer Engineering and Applications,2008,44(10):43-47. |
| |
| Authors: | GUO Wei MIAO Li ZHANG Dafang MIN Yinghua |
| |
| Affiliation: | 1.Software College，Hunan University，Changsha 410082，China 2.College of Computer and Communication，Hunan University，Changsha 410082，China 3.Institute of Computer Technology，Chinese Academy of Sciences，Beijing 100080，China |
| |
| Abstract: | Being an industry standard of software modeling language,UML is well accepted and extensively used in the industry.The UML Statechart describes some dynamic behavior of a system in its lifecycle.With systems to be modeled using Statechart become more and more large and complex,the Statechart often contain unexpected hidden dangers.It is then necessary to check the consistency and correctness.The paper presents an approach to model checking UML Statechart containing hierarchy and concurrent states.The software named SC2Spin is completed to check Statechart automatically.First semantics of Statechart is defined and then a new method to check Statechart is proposed,the Statechart is translated to Promela which is the input language of the famous model checking tool SPIN.To implement this method,this paper proposes Statechart Mountain Algorithm(SMA) to analyze the Translation in Statechart,proposes Translation Extraction to implement the translation.SC2Spin can detect errors like Deadlocks and Livelocks and verify LTL formulas. |
| |
| Keywords: | model checking Statechart Statechart Mountain Algorithm(SMA) Transition Extraction Spin |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
