基于事件确定有限自动机的UML2.0序列图描述与验证

• 作者: 张琛 段振华 田聪
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: UML2.0序列图 事件确定有限自动机 模型检测 命题投影时序逻辑 验证
• 年，卷（期）: 2011,（11）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 2625-2638
• 分类号: TP311
• 字数: 10691字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2011.04005

摘要

为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.