面向目标代码的实时操作系统形式化验证方法研究

作者：史建琦

来源：其他, 2012.

• 形式化验证
• 实时操作系统
• 目标代码
• 中间语言 Formal Verification
• Real-Time Operating System
• Binary Code Intermedi- ate Language

随着信息科学技术的飞速发展,基于实时操作系统构建的关键应用领域系统的正确性与安全性开始受到人们的广泛关注。由此,实时操作系统的正确性也愈发显得重要。为了确保实时操作系统的正确性与安全性,本文提出了面向目标代码的实时操作系统验证方法,并基于“核高基”重大科技专项课题“汽车电子系统可靠性分析和验证方法研究”中对实时操作系统ORIENTAIS的形式化验证工作,将提出的方法进行了实际应用。 本文从目标代码层面,对于实时操作系统的形式化验证工作,提出了相关的理论、方法与工具。在创新性方面,具体包括了如下几部分的内容： 一、面向嵌入式应用的目标代码中间语言xBIL 本文提出了面向嵌...

• 单位
  华东师范大学