Formal Specifications of Real-Time AUTOSAR-Compliant Operating Systems

Research output: Contribution to conferencePaperpeer-review

Abstract

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.
Original languageEnglish
Number of pages11
DOIs
Publication statusAccepted/In press - 7 Oct 2024
EventReal-Time Networks and Systems: RTNS 2024 - Critical Techworks, Porto, Portugal
Duration: 6 Nov 20248 Nov 2024
https://cister-labs.pt/rtns24/

Conference

ConferenceReal-Time Networks and Systems
Abbreviated titleRTNS
Country/TerritoryPortugal
CityPorto
Period6/11/248/11/24
Internet address

Fingerprint

Dive into the research topics of 'Formal Specifications of Real-Time AUTOSAR-Compliant Operating Systems'. Together they form a unique fingerprint.

Cite this