%0 Journal Article
%T 嵌入式操作系统的形式化验证研究
%A 陈丽蓉？
%A 李允？
%A 罗蕾？
%J 计算机科学
%D 2015
%X 描述了一个汽车电子嵌入式实时操作系统的分层形式模型:在低层,该操作系统的顺序内核承担基础设施的角色,实施任务、isr和系统服务等并发执行体之间的切换；而在高层,该操作系统向用户提供可并发执行的系统服务。两个层次的模型具有不同的配置状态视图和操作粒度。作为最重要的安全相关特性,应用与os之间的存储隔离保护机制在顺序内核的模型中得以体现。建立了操作系统的实现正确性定理,包括相应的仿真关系和实现不变量。根据该操作系统两个部分模型的特点及相应代码的实现语言情况,选择组合应用定理证明器isabelle/hol和程序验证工具vcc的方式,有效完成了该操作系统的形式化验证。
%K 嵌入式操作系统
%K 形式化验证
%K 建模
%K isabelle/hol
%K vcc
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=20150843&flag=1