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

摘要：

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

关键词：操作系统、存储保护、进程代数、PAT工具、形式化验证

所属期刊栏目：43

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金中丹合作项目6136113600;国家自然科学基金重点项目61532019;“核高基”重大专项2014ZX01038-101-001

在线出版日期：2017-08-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：79-85