支持汽车电子的状态图验证工具——Smart Automata

摘要

在汽车电子软件开发领域，基于模型的开发方式得到了越来越广泛的应用，而作为基于模型的开发方式的重要且不可或缺的组成部分，验证成为软件开发人员越来越关心的技术问题。本文探讨了如何利用对状态图的验证，来提高汽车电子软件的开发过程的效率和安全性。 本论文的研究目的是提供给用户一个支持状态图的可视化建模与动态模拟和验证的工具。通过该工具，可以帮助用户直观高效地对状态图进行建模，通过可视化的建模更好地实现软件开发过程中的沟通；并提供状态图的动态模拟仿真，帮助用户调试和发现建模的错误，和与预想的设计逻辑不相符合的地方，并且准确地定位到错误和问题的具体位置；最后通过状态图的验证来帮助用户在进行下一步软件开发前提早检查出可能出现的设计问题，从而使得用户能够更高效的完成汽车电子软件的开发工作。 本论文的主要贡献有： 1)在SmmOSEK IDE的框架中设计并实现了一个用户交互的状态图建模环境。能很好地为SmartOSEK IDE中支持汽车电子的状态图模型提供支持，也能够独立进行状态图建模。 2)针对状态图的模拟仿真，设计并实现了一个状态图语句的模拟器。通过在状态图仿真过程中，动态地在本机内存中模拟状态图中动作的执行，实时地保证状态图仿真的正确性。并且能够在模拟仿真过程前对状态图上的语句进行错误检查。 3)在状态图模拟的基础上，设计并实现了一个状态图的验证引擎。提供了状态图的验证功能，使用户可方便快捷地检查整体设计的逻辑正确性和其它的设计冗余问题。

目录

文摘

英文文摘

论文说明:图表目录

声明

第1章绪论

1.1研究背景

1.1.1基于模型的软件设计方法

1.1.2基于模型的验证方法

1.2论文的主要内容

1.3论文的主要贡献

1.4论文的组织结构

1.5本章小结

第2章背景与现状

2.1统一建模语言UML及状态图

2.2图形建模框架GMF

2.2.1图形编辑框架GEF

2.2.2 Eclipse建模框架EMF

2.3 Eclipse开发平台

2.3.1 Eclipse平台的体系结构

2.3.2 Eclipse中可扩展的插件机制

2.3.3 Eclipse的优势与特点

2.4相关产品分析

2.5本章小结

第3章状态图验证工具的设计与实现

3.1状态图验证工具的体系构架

3.2状态图建模环境

3.2.1状态图建模环境的功能

3.2.2状态图建模环境的系统结构

3.2.3状态图建模环境的设计与实现

3.3模拟仿真器

3.3.1声明信息的处理

3.3.2状态图的错误检查

3.3.3错误检查的设计与实现

3.3.4状态图的模拟仿真

3.3.5模拟仿真的设计与实现

3.4验证引擎

3.4.1验证界面与验证语言

3.4.2状态可达性的验证

3.4.3系统死锁的验证

3.5本章小结

第4章状态图验证工具的应用实例

4.1通过向导建立新项目

4.2状态图可视化建模

4.3状态图的模拟仿真

4.4状态图的验证

第5章总结与展望

5.1本文工作总结

5.2未来工作展望

参考文献

作者简介与在学期间主要研究成果

致谢