研究背景及意义
随着经济的发展和进步，计算机硬件性能不断提高，计算机技术和信息技术也越来越成熟，嵌入式系统在航空航天，交通汽车，核工业，医疗卫生等关键领域被广泛应用。这些嵌入式系统，不仅需要满足用户的基本功能需求，还需要具备较高的可靠性和安全性。如果嵌入式软件失效，可能会导致环境污染，财产损失，甚至是人员伤亡的严重后果[1]。例如：2019年3月10日，一架搭载157人的波音客机起飞6分钟左右即在埃塞俄比亚荒原坠毁，机上乘客无人幸存。造成这一惨剧的原因是737MAX的自动防失速系统（MCAS）存在问题，这一系统因回应错误的迎角信息而被启动，致使机头反复向下。737MAX失效导致的严重后果告诉我们：软件错误的控制系统会导致灾难性后果，软件的可靠性问题极为重要。所以保障软件安全性和可靠性是系统开发的重要部分。我们通过形式化方法来提高软件系统可靠性，建立有效的形式化方法可以为安全性分析提供支持。
形式化方法（Formal Methods）是软件工程中提高系统可靠性的一种重要方法。形式化方法是以数学为基础的用以对系统进行说明、设计和验证的语言、技术和工具的总称。形式化方法可以在不同抽象层次上描述整个或部分系统行为的规约和模型。虽然我们无法确保系统是百分之百安全的，但是我们可以借助于形式化方法，极大地提高系统的可靠性程度。
接口自动机是一种用于构件组合的形式系统。2001年由Luca de Alfaro和Thomas A. Henzinger正式提出的接口自动机与其他形式化工具最大的区别是“乐观方法”和博弈思想。乐观方法用来定义开放式系统中的接口兼容问题，博弈思想是描述这一问题的语义[2]。接口自动机（Interface Automat IA）是一种轻量级的描述构件接口行为的状态机模型，用于描述构件接口的时序特性。构件接口是构件功能的外部表现，接口可屏蔽构件间差异，是嵌入式构件组装和重用的基础。ＩA模型可描述构件间的数据通信过程，外部行为特性等，是嵌入式构件建模的有效工具[3]。
状态事件故障树[4]（State/Event Fault Tree, SEFT）是一种描述系统中失效因果链的建模技术，其顶层事件描述失效发生的结果，对顶层事件发生的平均时间进行分析，是获得系统平均失效时间参数的一种有效方法[5]。由于状态事件故障树是半形式化模型，不具有严格的语义，需要定义其形式化语义才能够进行分析。
交互马尔可夫链（IMC）是一种描述系统的性能和功能的混合模型，定义了描述构件组合行为语义和弱互模拟操作。在系统功能描述的基础上加入性能指标、常用于系统的功能验证和性能评价。IMC可以同时描述构件行为和概率信息。通过将交互马尔可夫链模型的交互语意精化为输入、输出动作，提出接口交互马尔可夫链模型（Interface-IMC）用于状态事件故障树（SEFT）的形式化语义描述。
从软件工程的观点分析，目前软件开发前期缺乏足够的工具对系统设计的概率行为进行有效的分析与检验，使得软件后期的开发和维护比较困难。基于形式化方法的软件验证工具可以在软件开发的设计阶段，对系统重要性质进行有效的分析和验证。本课题目的是基于弱互模拟操作对接口交互马尔可夫链的聚合算法进行分析和实现，并以图形化形式实现和展示聚合算法。
- 国内外研究概况
目前，国内外在嵌入式软件安全性分析方面已经进行了广泛的研究工作，嵌入式软件安全性方面的研究工作一般分为以下五个方面：危害分析、软件安全需求的提取与分析、软件安全性设计、软件安全验证和确认、软件安全认证及标准。已有的研究工作已对软件安全性分析的这些方面进行了相关的研究工作。
- 软件可靠性
软件可靠性是软件工程与可靠性工程结合产生的前沿科学，指对于规定环境，在给定事件内软件无失效运行的概率[6]。目前针对软件可靠性的预测主要是对构件间的连接进行概率建模，然后用离散/连续马尔可夫链（Discrete/Continuous Time Markov Chain, D/CTMC），随机Petri网（Stochastic Petri Net, SPN）或有向无环图（Directed Acyclic Graph）来预测软件系统的可靠性[7]。
以上是毕业论文文献综述，课题毕业论文、任务书、外文翻译、程序设计、图纸设计等资料可联系客服协助查找。
