来源：ercim
The integration of different dependability techniques is an open research question. We address problems that arise when attempting to combine fault tolerance mechanisms with formal methods and formal verification tools in the development of an embedded system.
对具有不同可靠性的技术进行综合应用是一个正处于研究中的课题。我们将阐述当在嵌入式系统的开发过程中尝试将容错机制与形式化方法和形式化验证工具结合起来的时候所产生的问题。
近些年来，人类在生活中所依靠的各种嵌入式系统的广泛普及已经引起了很多安全方面的关注。错误预防、容错、错误消除与错误预报相结合的技术已经广泛应用以获得高度的可靠性。然而，在不同技术的整合方面却没有一个统一的标准和方法。比如，具有不同背景和应用场合的工业部门会在采用意在提高可靠性的技术时遵循他们各自独特的开发模式。
采用具有严格的定义、功能分析与系统表现的形式化方法意味着系统是按照一组预先定义的抽象属性进行设计的，这样可以保证其能够产生“正确的”行为。如此看来，这些对于系统安全要求严格的工业部门采用的形式化方法竟然是如此之少实在令人吃惊，尽管现在使用这些系统要越来越多的遵守系统开发的国际标准与框架。事实是：工业领域形式化方法的普遍采用与引入这些方法所需的投资，现有支持工具的成熟度，以及易用性等方面都紧密相关。由于以上这些原因，现今工业领域的趋势是采用形式化的验证技术以在现有的开发过程中检验系统设计与整合的有效性。工业领域比较倾向于在使用形式化的验证技术来评估他们产品的质量特性时采用传统的生命周期，而不是采用形式化的全生命周期开发模式，原因很简单：这样在成本上会便宜一些。
几种在开发过程中应用形式化方法的建议已经被提了出来；它们之间主要的差别在于包含形式化方法的程度不同。具有严格规范的形式化方法可以用作生成测试用例，作为一种确认技术，目的是证明规格参数符合要求，或者只是在代码的自动生成中作为一种辅助技术。
基于模型检验的形式化验证方法被应用于对系统行为的一种有限状态表示上面。验证过程通常是通过使用模型检验算法表明特定属性的可满足性来实现的，而这些属性则被形式化为关于系统模型的逻辑方程。比如，安全和活性要求可以表示为时域的逻辑方程并可以在系统模型上进行检测。不幸的是，这种方法受到所谓的“状态空间爆炸”问题的影响，当系统由几个子系统组成时问题就会出现。在这种情况下，产生的有限状态模型所包含的状态数量与子系统部分的数量呈指数关系。严格依赖于数据值的系统面临着同样的问题，产生的状态数量与数据变量的数量呈指数关系。因此，传统的模型检验技术就被证明对于许多现实中的系统来说不够强大，这些系统的模型中包含着多于100000个的状态。
但是，最近模型检验技术的发展已经可以通过在模型检验器中使用符号处理算法来处理非常庞大的状态空间。这样的工具已经在硬件验证领域具有庞大状态空间的应用场合下取得了成功。
嵌入式计算机控制系统中通常包含了容错技术。容错是一种由系统通过冗余机制提供的使其在发生错误时依然能够按照规范进行运作的性质。严格的定义和验证对于这类系统来说极其重要，因为它使系统在出现错误甚至失败时依然显示其正确性成为可能。
图：嵌入式计算机控制系统中通常包含了容错技术，铁路联锁系统就是一个实例
我们已经将模型检测验证技术应用到了嵌入式系统上，以说明嵌入式系统中特定的特性，比如冗余的使用，是如何帮助减少状态空间爆炸问题的。在这一工作过程中，我们考虑了几种研究实例。两个有趣的例子是对于由Ansaldo Trasporti公司开发的铁路联锁系统安全要求的验证和对欧盟工程GUARDS（Generic Upgradable Architecture for real-time Dependable Systems，实时可靠系统的一般可升级结构）内部定义的一些容错机制的验证。
对两个实例的研究都表明：
模型检测的形式化验证方法的应用是可行的，并且已经很好的被包含嵌入式容错系统的工业场合所接受。
形式化的过程严格的依赖于应用的领域。一些用于从半形式化的系统描述到其形式化规范转变的标准规则可以成功的应用于嵌入式容错系统的领域之中。这种转变通常被认为是在软件开发周期中引入形式化方法的关键点之一。
由冗余系统的相结构所带来的状态空间的减少使模型检测方法在其应用领域成为可行。
作为规范语言使用的有限状态模型在确保形式化规范与最初的半形式化规范的一致性方面具有优势。