关键词:
同步语言
形式化方法
CCSL
标记迁移系统
安全性分析
摘要:
随着安全关键嵌入式系统广泛运用在航空航天,交通运输,核电核能等领域,软件安全越来越多的影响人们的生命和财产安全。与此同时,此类软件对系统效率,资源利用,响应时间,多时钟属性和安全相关性质等有着更高的要求。如何对此类系统进行设计与分析,成为学术界和工业界的热点研究问题。随着系统的复杂性不断增加,对于具有多时钟性质的此类系统需求日益增加。同步语言SIGNAL是一种声明式数据流同步设计语言,多时钟的同步语言SIGNAL适合建模具有多时钟性质的嵌入式反应系统,丰富的表达能力也给此类系统行为的安全性验证带来了困难。基于形式化方法的仿真和检测分析能够为软件的开发与验证提供严格保障。本文基于形式化的方法,考虑多时钟嵌入式反应系统,针对SIGNAL模型难以在设计阶段发现系统缺陷的问题,本文提出的方法可以分别从仿真验证和有界性检测两个侧面对系统进行分析,以达到在系统设计的初期,发现系统中存在的危险,并反馈给系统设计者。论文主要研究内容包括:(1)提出基于CCSL时钟限制规约的SINGAL模型的时序行为仿真分析方法。首先,我们将源模型SIGNAL设计的多时钟嵌入式系统模型转换至CCSL时钟模型,利用CCSL的可执行语义,对系统的时序行为进行仿真。此外,还可加入硬件执行平台信息,给出软硬件仿真结果。(2)提出基于标记迁移系统的SIGNAL模型的有界性检测分析方法。设计了SIGNAL模型中操作结构的状态变迁语义系统,基于此系统构建系统行为的状态自动机。针对多时钟系统所关心的有界性问题,我们给出了基于标记迁移系统的有界性检测算法。(3)最后使用本文提出的分析方法对一个自动驾驶系统的控制模块进行案例分析,从SIGNAL系统建模开始,分别从仿真分析和有界性检测两个侧面,找出系统中存在的安全性隐患,说明了本文方法的有效性和可行性。