论文部分内容阅读
随着信息科学技术的飞速发展,基于实时操作系统构建的关键应用领域系统的正确性与安全性开始受到人们的广泛关注。由此,实时操作系统的正确性也愈发显得重要。为了确保实时操作系统的正确性与安全性,本文提出了面向目标代码的实时操作系统验证方法,并基于“核高基”重大科技专项课题“汽车电子系统可靠性分析和验证方法研究”中对实时操作系统ORIENTAIS的形式化验证工作,将提出的方法进行了实际应用。本文从目标代码层面,对于实时操作系统的形式化验证工作,提出了相关的理论、方法与工具。在创新性方面,具体包括了如下几部分的内容：一、面向嵌入式应用的目标代码中间语言xBIL本文提出了面向嵌入式应用的目标代码中间语言xBIL(eXtensive Binary Internediate Languag)。xBIL可对多种平台架构上的目标代码进行统一形式的表示。xBIL支持中断行为描述,可对包括操作系统在内的底层程序的中断行为进行表示。xBIL支持指令执行时间声明,并可对程序的执行时间进行评估。本文给出了xBIL语言的操作语义与指称语义,并对两种语义进行了语义等价性证明。二、基于目标代码中间语言xBIL的位域运算与判定过程在基于目标代码的应用环境下,xBIL语言需要新的位域运算与判定过程对其执行行为进行判定。本文提出了新的基于目标代码中间语言xBIL的位域运算规则与判定过程。三、基于目标代码的实时操作系统验证方法本文提出了针对实时操作系统目标代码的形式化验证方法。针对实时操作系统给出了其在目标代码级的形式化验证流程与相关方法以及操作系统功能性规范的验证方法。并结合中断发生概率,提出了操作系统在带中断程序条件下的内存访问安全性质验证方法与操作系统API边界响应时间的计算方法。四、基于目标代码的自动化集成验证平台本文工作设计实施了一种自动化集成验证平台。集成验证平台可提供多种验证工具,工具可通过服务总线适配器与总线进行连接,从而实现对操作系统目标代码的自动化集成验证。通过上述的方法与技术,在实践过中,对ORIENTAIS操作系统进行了形式化验证工作,也从侧面证实了本文方法的实用性。通过对本文方法发现的国产汽车电子实时操作系统ORENTAIS中的37项错误的改进,ORIENTAIS顺利通过国际OSEK标准组织认证。