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

• 作者: 李允 罗蕾 陈丽蓉
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 嵌入式操作系统 形式化验证 建模 Isabelle/HOL VCC
• 年，卷（期）: 2015,（8）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 203-214
• 页数: 12页
• 分类号: TP316.2
• 字数: 16120字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2015.8.043

摘要

描述了一个汽车电子嵌入式实时操作系统的分层形式模型:在低层,该操作系统的顺序内核承担基础设施的角色,实施任务、ISR和系统服务等并发执行体之间的切换;而在高层,该操作系统向用户提供可并发执行的系统服务.两个层次的模型具有不同的配置状态视图和操作粒度.作为最重要的安全相关特性,应用与OS之间的存储隔离保护机制在顺序内核的模型中得以体现.建立了操作系统的实现正确性定理,包括相应的仿真关系和实现不变量.根据该操作系统两个部分模型的特点及相应代码的实现语言情况,选择组合应用定理证明器Isabelle/HOL和程序验证工具VCC的方式,有效完成了该操作系统的形式化验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李允	电子科技大学计算机科学与工程学院	25	207	9.0	13.0
2	罗蕾	电子科技大学计算机科学与工程学院	58	583	14.0	21.0
3	陈丽蓉	电子科技大学计算机科学与工程学院	11	149	5.0	11.0