- 研究背景及意义
- 课题背景
随着嵌入式软件规模的迅速发展，软件系统的复杂度也越来越高，使软件对整个系统的影响逐渐占据了统治地位，人们所需考虑的层面也越来越抽象。从军事领域的航母战斗群、作战机到民用领域的汽车、核电站,从耗资巨大的航天飞机到小小的家用电器,都是如此。更不要说信息化带来的无处不在的虚拟网络世界。在这些系统中,软件的失效往往给我们带来无可挽回的财产损失甚至是人员的伤亡。这就促使我们加快研究提高软件可靠性的可信度方法。现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术的支撑。其中，模型就是对复杂问题进行分层，建模是对系统进行抽象的最好的办法，从而更好地解决问题。因此，软件系统建模在整个软件工程中也越来越重要。
UML自上世纪90年代产生至今，作为基于面向对象技术的标准建模语言，已经被广泛使用。UML是一种定义良好、易于表达、功能强大且普遍适用的建模语言，主要用来对软件系统进行可视化建模。UML的优势主要体现在它可以使用单一的集成表示法来对系统的多个方面进行建模，可以用于描述一个系统的静态结构和动态行为。静态结构定义了系统中对象的属性和操作，以及这些对象之间的相互关系。动态行为定义了对象在时间上的特性和对象间的交互机制。
其中，UML顺序图反映的是系统中并发对象之间的消息交互，是UML建模语言的核心元素之一，其使用非常广泛。然而由UML得到的表示系统多个方面的模型之间存在着一定的信息冗余和相互交织，从而产生了一致性问题。在设计大型系统的模型时保持一致性是比较困难的，一个含有错误设计的模型在软件设计和开发的过程中被使用，严重的会造成整个软件项目的失败。因此，这就要求我们在软件的设计阶段就对设计模型进行验证。
由于嵌入软件不仅具有极高的可靠性，还有严格的实时性要求，使得实时系统除了要保证任务完成的逻辑正确性，同时也要保证任务完成的时间正确性。故而实时系统经常被用于对时间特性有要求的关键性领域当中，而针对这些领域，若能在软件开发的早期阶段发现软件错误，即可节省大量的人力和财力在后期的修理和维护中[1]。模型检验是一种产生于上世纪80年代的形式化验证技术，目前该技术已经相当成熟。模型检测技术能够将系统的验证问题转化为数学问题来解决。这种用严格的数学方法来推理验证某一产品或设计是否符合其全部或部分规范的技术，可以很好的应用于高可信软件系统的实现过程中。同时，UML顺序图规约一致性验证算法的实现与分析，对于软件开发、保证需求分析的正确性是至关重要的。基于UML模型顺序图规约一致性的测试长久以来一直是国内外一些软件工程相关领域的研究热点。
目前，工业界已有一些比较有效的嵌入式软件测试和调试方法[2]（如：在处理器中嵌入ICE功能，调试代理软件，JTAG模拟等）。但从软件工程的角度看，这些传统的嵌入式软件可靠性保障技术主要关注于系统开发后期，而在系统设计前期缺乏有效工具对系统设计的功能性质以及非功能性质进行分析与验证。
2.研究目的和意义
在一个软件系统的开发过程中，建模设计是重要的环节。就开发成本而言，除了自身的成本外，后期的实现和维护的成本也是不可忽略的重要部分。如果一个错误在设计阶段没有发现和纠正，在软件交付后维修他的成本将是原来的5至100倍[3]。所以，前期的模型设计是软件开发过程中至关重要的一个环节，并且一个完整的系统模型也是进行形式化分析和验证的基础。形式验证的思想是,通过对系统是否满足某类性质作出确定性的判断和回答来获取更高的系统可信度。其本质上就是判断系统实现是否与系统规范一致的过程。其中，模型验证方法就是形式化验证方法中的一种。对于具有高可靠性需求的嵌入式软件系统而言，建立有效的应用于软件设计与分析的前期阶段的形式验证工具有非常重要的意义。因此，本课题之所以关注软件前期设计的验证而不是后期软件的测试,是因为在设计阶段进行形式验证有助于尽早发现错误、减小纠正的代价，并且软件设计对系统的抽象层次一般比较高,便于形式验证方法的应用。
本课题研究的最终目的是将此研究成果可以应用于构件化嵌入式软件开发的设计建模阶段，不仅可以对关键功能性质进行验证，还可以对非功能性质进行严格形式化分析和验证，从而提高系统可靠性的可信度。
- 国内外研究概况
由于嵌入式系统通常由多个子系统构成，其软件系统具有较高的构件化特征[4]，构件之间的交互场景是体现系统行为复杂性的一个重要方面。作为一种描述构件接口性质的形式化语言，接口自动机刻画了构件以及外部环境之间交互行为的时序特征，可以用来对构件化嵌入式软件的行为进行有效的建模与分析。
以上是毕业论文文献综述，课题毕业论文、任务书、外文翻译、程序设计、图纸设计等资料可联系客服协助查找。
