Formal Modeling And Analysis Of AUTOSAR Memory Protection Mechanism

With the expansion of the production scale, AUTOSAR (AUTomotive Open System Architecture) standard, which is based on open system architecture, is becoming more and more popular. Research in AUTOSAR memory protection mechanism is gradually thorough. And how to improve the safety of auto memory protection standard is a problem worthy of studying.In this paper, we adopt the modeling language CSP to formalize the memory protection mechanism and the operation mechanism of applications based on AUTOSAR specification. With the purpose of verify the conformance between the specification and the model, we employ the model checker PAT to simulate the model and verify whether it satisfies some certain properties, such as dead lock-free, safe and liveness properties, which are extracted from the specification and described as LTL formulas.Modeling AUTOSAR memory protection mechanism by formal method can guarantee its security. Furthermore, it provides a trustable support for the security of automotive electronic operating system by logically discussing the importance of AUTOSAR memory protection mechanism.