论文部分内容阅读
随着计算机技术的迅速发展,嵌入式系统在医疗、交通、通信、航空航天等安全关键领域已得到广泛运用。如何提高系统的安全性,防止灾难性事故发生,已经成为当前软件工程领域重要的研究课题。AltaRica语言是一种描述正常情况下系统功能行为,同时描述系统存在的失效行为的建模语言,面向AltaRica模型的系统安全性分析是当前的研究热点之一。目前已有相应的一些工具利用AltaRica模型进行系统安全性分析,而支持AltaRica模型的穷举分析和时序属性方面的验证工具还很缺少,成熟的模型检测工具SPIN对模型的穷举分析和线性时序逻辑验证有很大优势,但SPIN工具并不能直接对AltaRica模型进行验证。针对以上问题,本文首先将AltaRica模型转换到Promela模型,对安全需求使用线性时序逻辑进行规约;然后将Promela模型导入模型检测工具SPIN进行验证和分析;最后结合验证结果和可追踪性信息模型,追踪AltaRica模型存在的设计缺陷。本文的主要研究内容如下:第一,通过对AltaRica模型和Promela模型的语义分析,提出了AltaRica模型到Promela模型的转换规则,并对两模型语义的等价性进行证明。使用线性时序逻辑对安全性需求进行规约并结合转换得到的Promela模型导入模型检测工具进行形式化验证。在此基础上,提出一种面向AltaRica模型的系统安全性设计验证方法。第二,针对模型检测的验证结果,给出了根据验证结果的反例路径追踪到AltaRica模型设计缺陷的可追踪性信息模型。通过对验证结果和AltaRica模型的分析,首先给出验证结果可追踪性信息模型的元模型;然后根据具体的追踪目标实例化元模型,得到可追踪性信息模型;最后基于可追踪性信息模型设计追踪算法,实现根据验证结果的反例路径追踪查找AltaRica模型的设计缺陷甚至系统组件存在的安全性问题。第三,针对本文提出的面向AltaRica模型的系统安全性设计验证方法,设计并实现相应的原型工具A2STool,对A2STool的功能模块进行相应地说明,并给出该工具的设计框架、执行流程以及关键的实现技术。最后,运用本文提出的方法对机轮刹车系统控制单元进行案例分析,利用原型工具给出了AltaRica模型到Promela模型转换的完整过程,使用SPIN对Promela模型和安全性需求的线性时序逻辑规约进行验证和分析,接着基于验证结果结合可追踪性信息模型发现系统安全性设计缺陷。说明了本文方法的有效性和可行性,为系统的安全性分析提供了一种新思路。