摘要： 传统汽车标准存储模块的安全性较低,汽车电子操作系统在访问存储模块时会出现访问越界和数据冲突等问题。为此,提出一种操作系统的存储保护机制。运用进程代数给出满足存储保护机制的形式化验证框架,从逻辑上讨论AUTOSAR存储保护机制的重要性,使用进程代数方法对该机制建立形式化模型,并根据AUTOSAR规范,抽取无死锁性、安全性、活性等性质,运用模型检验工具PAT实现该模型,并对各个存储模块的读写访问性质进行验证。仿真结果表明,与传统的汽车标准相比,该机制符合AUTOSAR OS规范,具有较高的安全性。
关键词:
操作系统,
存储保护,
进程代数,
PAT工具,
形式化验证
Abstract: Since the security of standard storage module of traditional vehicle is relatively low,problems like accessing out of bounds or data conflicting may occur while the electronic operating system of vehicles accesses the storage modules.So a storage protection mechanism of operation systems is proposed.The process algebra is used to give the formal verification framework that ensures the storage protection mechanism,and the importance of the AUTOSAR storage protection mechanism from the logical point of view is discussed.A formal model of the mechanism is built using process algebra,and the properties like deadlock freeness,safety and liveness are extracted according to the AUTOSAR specifications.Then the model is implemented using PAT——a modelling and verification tool for process algebra,and the correctness of read-write properties of each storage module is checked.Simulation result shows that compared with conventional car standard,the mechanism conforms with the AUTOSAR OS specification and has higher security.
Key words:
operating system,
storage protection,
process algebra,
PAT tool,
formal verification
中图分类号: