Formal Specifications of Real-Time AUTOSAR-Compliant Operating Systems

The \textbf{AUT}omotive \textbf{O}pen \textbf{S}ystem \textbf{AR}chitecture (AUTOSAR) is a set of documents that provide guidance for implementing automotive software. The Software Specifications of the Operating System (SWS\_OS) standardizes interfaces and functional requirements for an AUTOSAR-compliant OS. Merely implementing the required interfaces is not sufficient to demonstrate AUTOSAR compliance; it is important to show that the interaction between interfaces meets the functional requirements outlined in the SWS\_OS.

This paper introduces a method for formally specifying and verifying that a given implementation meets the SWS\_OS specifications. Our approach involves formally defining the functional requirements and using formal reasoning to demonstrate that an implementation adheres to these requirements. We have applied this method to a widely-used real-time operating system (RTOS) to prove its compliance with AUTOSAR by ensuring that it satisfies the necessary functional properties.