Formal Specifications of Real-Time AUTOSAR-Compliant Operating Systems

The AUTomotive Open System ARchitecture (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.