AUTOSAR OS存储保护机制的形式化验证框架

• 作者: 朱晓冉 李青 郭建
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 操作系统 存储保护 进程代数 PAT工具 形式化验证
• 年，卷（期）: 2017,（1）
• 所属期刊栏目: 体系结构与软件技术
• 页码范围: 79-85
• 页数: 7页
• 分类号: TP311
• 字数: 6558字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2017.01.014

摘要

传统汽车标准存储模块的安全性较低,汽车电子操作系统在访问存储模块时会出现访问越界和数据冲突等问题.为此,提出一种操作系统的存储保护机制.运用进程代数给出满足存储保护机制的形式化验证框架,从逻辑上讨论AUTOSAR存储保护机制的重要性,使用进程代数方法对该机制建立形式化模型,并根据AUTOSAR规范,抽取无死锁性、安全性、活性等性质,运用模型检验工具PAT实现该模型,并对各个存储模块的读写访问性质进行验证.仿真结果表明,与传统的汽车标准相比,该机制符合AUTOSAR OS规范,具有较高的安全性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭建	华东师范大学计算机科学与软件工程学院	5	11	2.0	3.0
2	李青	华东师范大学计算机科学与软件工程学院	9	47	4.0	6.0
3	朱晓冉	华东师范大学计算机科学与软件工程学院	2	4	2.0	2.0