基于实时接口自动机的构件化系统组合与验证工具的实现开题报告

1. 研究目的与意义

随着实时系统的发展，嵌入式软件实时行为的分析与验证一直是实时计算领域中的重要内容。

由于实时系统本身的复杂性，以及uml与其在嵌入式实时方面的扩展建模语言已经开始得到广泛应用，人们希望能够在这些图形化的建模语言基础上进一步研究表达能力更强的时间约束形式，并在系统设计阶段能够对系统设计模型与规约模型之间的实时一致性进行严格的分析和验证。

本课题研究的目的是将此研究成果可以应用于构件化嵌入式软件开发的设计建模阶段，对关键功能性质进行验证，使得设计者可以尽早在系统开发前期发现错误并予以修改，以降低成本并提高系统可靠性的可信度。

2. 国内外研究现状分析

目前，国内外已经有了一些较有影响的模型一致性检验工具，如SPIN、Chic、UPPAAL、Ticc、Ptolemy II等工具。

这些研究成果可以在系统模型设计的前期，通过应用一些形式化一致性验证方法，帮助设计者判断系统规约与建模设计之间是否一致，及时指出不一致所在，从而很大程度上提高软件系统的可靠性。

3. 研究的基本内容与计划

研究内容：一、分析项目背景及国内外研究的最新发展趋势二、输入输出接口设计三、UML顺序图模型的预处理四、接口自动机组合模型的建立与实现五、实时功能行为验证的实现进度计划：序号 项目 时间 阶段成果1 研究背景和发展趋势 2-4周 文献综述，开题报告2 选择并搭建开发环境 1-2周 开发计划，技术方案3 实现功能并完成测试 4-8周 项目源码，代码文档4 撰写论文并准备答辩 2-4周 毕业论文，答辩文稿

4. 研究创新点

一、以带时间约束的UML顺序图作为系统的规约说明，选用实时接口自动机作为系统的设计模型二、可以对嵌入式软件系统的实时行为进行分析和验证