嵌入式操作系统的形式化验证研究  

Research on Formal Verification of Embedded Operating System

作　　者：陈丽蓉[1] 李允[1] 罗蕾[1] 

机构地区：[1]电子科技大学计算机科学与工程学院,成都611731

出　　处：《计算机科学》2015年第8期203-214,共12页Computer Science

基　　金：国家自然科学基金项目(61401067);四川省应用基础研究项目(2013JY0002)资助

摘　　要：描述了一个汽车电子嵌入式实时操作系统的分层形式模型:在低层,该操作系统的顺序内核承担基础设施的角色,实施任务、ISR和系统服务等并发执行体之间的切换;而在高层,该操作系统向用户提供可并发执行的系统服务。两个层次的模型具有不同的配置状态视图和操作粒度。作为最重要的安全相关特性,应用与OS之间的存储隔离保护机制在顺序内核的模型中得以体现。建立了操作系统的实现正确性定理,包括相应的仿真关系和实现不变量。根据该操作系统两个部分模型的特点及相应代码的实现语言情况,选择组合应用定理证明器Isabelle/HOL和程序验证工具VCC的方式,有效完成了该操作系统的形式化验证。A layered formal model for an automotive embedded real-time operating system was presented. At the lower layer,the sequential kernel plays the infrastructural role in executing switching between concurrent entities such as tasks, ISRs and system services, and at the higher layer the concurrent system services are provided to users. The two layers of the model have different views of configurations and operation granularities. As the most important safety related feature, the memory isolation and protection mechanism between applications and the OS is modeled in the sequen- tial kernel. The implementation correctness theorem of the OS was established along with the corresponding simulation relation and implementation invariants. According to the features of the model and the related implementation langua- ges,the OS was formally and effectively verified with a combined usage of the theorem prover Isabelle/HOL and the program verifier VCC.

关 键 词：嵌入式操作系统 形式化验证 建模 Isabelle/HOL VCC 

分 类 号：TP316.2[自动化与计算机技术—计算机软件与理论]