论文部分内容阅读
嵌入式软件已广泛应用于航空航天、核工业、交通等领域,且嵌入式软件已成为决定系统安全的主要因素。如何保障软件安全性已成为学术界和工业界的重点问题。针对软件安全需求进行分析,以及针对软件功能进行设计,是软件安全性分析的主要关注点,但二者在实际开发中通常是独立进行的,致使在软件功能设计中,难以参照软件安全需求分析结果进行修改,软件安全需求分析难以在软件功能设计阶段进行,且基于软件功能设计模型难以开展软件安全性分析工作。已有基于故障树的安全性分析无法描述软件的组件行为,且故障树分析不能在软件功能模型设计中确定是否存在故障之间的因果关系,而基于状态图的软件设计模型能够描述软件的行为,但是难以发现其中隐藏的故障隐患。针对以上问题,本文提出了一种基于状态事件故障树(State/Event Fault Tree,SEFT)的软件安全性分析方法,使用SEFT(State/Event Fault Tree,SEFT)描述软件发生的故障因果关系及导致故障的组件内部行为,再提取安全需求规约,并将其扩展到状态图,最后通过模型检测方法对扩展模型进行安全性验证与分析。论文主要研究内容如下:(1)使用SEFT描述软件故障及导致软件故障的组件内部行为,并使用线性时序逻辑将其时序化,得到时序状态事件故障树(Liner Temporal SEFT,LTSEFT),根据约简规则将其约简,最后根据其最小割集提取LTL(Linear Temporal Logic)规约。(2)定义了SEFT逻辑门到状态图元素的转换规则,设计了安全需求到状态图元素的安全需求信息映射表,以及基于映射表和转换规则自动构建系统安全需求扩展状态图的算法。(3)通过模型转换,将扩展的状态图转换到Promela,输入到SPIN中,根据提取的安全属性LTL规约进行安全性验证和分析。最后,运用本文提出的方法对襟缝翼控制系统进行案例分析。给出了构建系统SEFT(State/Event Fault Tree,SEFT)及LTSEFT(Liner Temporal SEFT,LTSEFT)的过程,提取LTL(Linear Temporal Logic)规约,并对转换得到的Promela进行验证和分析,说明了本文方法的有效性,为嵌入式软件安全性分析工作提供了一种新思路。