基于Spin的UML状态图模型检查的设计与实现

作     者：郭伟 缪力 张大方 闵应骅 GUO Wei;MIAO Li;ZHANG Dafang;MIN Yinghua

作者机构：湖南大学软件学院长沙410082 中国科学院计算技术研究所北京100080 

基　　金：国家部委基础科研“十一五”项目 国家自然科学基金(the National Natural Science Foundation of China under Grant No.60673155) 

出 版 物：《计算机工程与应用》 (Computer Engineering and Applications)

年 卷 期：2008年第44卷第10期

页      码：43-47页

摘      要：UML已经是软件建模方面的标准语言,UML Statechart描述了系统在其生命周期中的动态行为。随着系统规模的扩大和复杂度的提高,Statechart往往包含设计者所未预料到的隐患,通过模型检查来对Statechart进行穷举检验就成为一个重要课题,首先给出了含层次、并发Statechart的语义;随后提出了对Statechart进行模型检查的一种新方法,并且已经编写软件SC2Spin实现此方法,该方法使用了提出的Statechart山脉算法和迁移提取法,可以将一个Statechart自动转化为Spin的输入语言Promela,从而验证Statechart的死锁、活锁等错误和时序逻辑公式。

主 题 词：模型检查 Statechart Statechart山脉算法 迁移提取 Spin 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3778/j.issn.1002-8331.2008.10.013

馆 藏 号：203325613...