嵌入式系统 | 基于SCADE模型的形式化方法

在上期嵌入式系统专题内容中，针对Ansys SCADE的诞生、发展及应用做了详细梳理。本文将重点阐述“基于SCADE模型的形式化方法”，做个通俗的比喻，形式化方法就是将程序抽象为一个数学公式，然后用严密的数学推理来证实或证伪该公式。在当下软件行业已经有众多测试手段的前提下，为什么还需要形式化方法呢？除非对程序进行的测试能够穷尽所有可能的场景，否则传统的测试手段无法完全保证系统的安全可靠。可以说，唯有形式化方法才能从根本上确保系统的安全可靠，而这一点在安全关键的系统中尤为重要。目前，形式化方法在详细设计层面，对于软件行为等模型较为适用。