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

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

嵌入式系统将助力新技术的发展

嵌入式计算系统应用极其广泛，遍及各行各业，总市场规模非常巨大。IDC将嵌入式系统的民用应用领域划分为六个主要行业：汽车、工业、医疗、能源、通信、消费电子。其中，通信和消费电子是目前最大的两个行业，而能源行业则是增长最快的行业。全球嵌入式系统市场 2013 年达到 1403.2 亿美元，预计到 2020 年将达到 2,143.9 亿美元，年复合增长率达 6.3%。据了解，目前嵌入式现状是核心技术的国产化程度不高、存在很强的发展诉求；嵌入式计算供应商以国外和台湾地区厂商为主；国内嵌入式计算市场的技术服务能力更为重要。目前已经与1800多家企业签订了长期合作协议，其中包括10多家世界500强企业。