活性顺序图规约到时间博弈自动机模型的转换方法研究与工具实现

摘要

活性顺序图(Live Sequence Chart,LSC)是一种基于场景的形式规约语言，可以直观且精确地刻画系统构件间的交互行为，常用于反应式系统开发的需求分析。由于在多个场景描述间容易产生逻辑矛盾，因此在对系统模型求精(refinement)前，必须验证确保系统的LSC规约是一致的。
　　为了有效地判定规约的一致性，本文主要研究了一种LSC规约的形式化综合方法，该方法通过将LSC规约等价地转换到时间博弈自动机(Timed Games Automata)模型，把LSC规约的一致性检测问题转化为时间博弈解决工具UPPAAL-TIGA中计算系统获胜策略的问题。主要研究成果如下：
　　(1)针对LSC规约到TGA模型的等价转换问题，本文研究了LSC中的Instance、Cut、Event和UPPAAL-TIGA工具中TGA的Process、Location、Edge的语义等价性，给出了从LSC规约到TGA模型的转换规则和算法描述。
　　(2)针对LSC模型文件到UPPAAL-TIGA模型文件的自动转换问题，本文分析了模型文件转换处理的具体流程，解析了LSC-editor工具的lsc文件和UPPAAL-TIGA工具的xml文件，给出了LSC和TGA中各语义的数据结构，基于：
　　(1)的转换算法，最终实现了一个模型转换工具LSC-to-TGA。
　　(2)研究了一个道岔自动控制系统的应用实例，分析了故障容错和超速防护场景下的系统需求并给出了LSC规约，使用LSC-to-TGA转换工具将LSC规约转换为时间博弈自动机模型，对TCTL公式描述的系统获胜条件使用UPPAAL-TIGA工具计算系统的获胜策略，结果表明系统的LSC规约是一致的。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

§1.1 研究背景及意义

§1.2 国内外研究现状

§1.3 研究内容

§1.4 章节安排

第二章 时间博弈自动机与活性顺序图

§2.1 时间博弈自动机

§2.2 活性顺序图

§2.3 本章小结

第三章 从LSC规约到TGA模型的转换规则和算法

§3.1 相关工作

§3.2 实例分析

§3.3 转换规则和算法描述

§3.4本章小结

第四章 LSC-to-TGA模型转换工具的设计与实现

§4.1 LSC-to-TGA的设计

§4.2 具体实现

§4.3 本章小结

第五章 道岔自动控制系统实例研究

§5.1 应用背景和相关工作

§5.2 道岔自动控制系统和场景描述

§5.3 道岔自动控制系统的LSC模型

§5.4 模型转换

§5.5 获胜策略计算

§5.6 本章小结

第六章 结束语

§6.1 主要研究工作总结

§6.2 存在问题及研究展望

参考文献

致谢

攻读硕士学位期间发表或录用的论文