Abstract
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.
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 language | English |
|---|---|
| Title of host publication | RTNS 2024 - 2024 32nd International Conference on Real-Time Networks and Systems |
| Publisher | Association for Computing Machinery (ACM) |
| Pages | 187-196 |
| Number of pages | 10 |
| ISBN (Electronic) | 9798400717246 |
| DOIs | |
| Publication status | Published - 3 Jan 2025 |
| Event | 32nd International Conference on Real-Time Networks and Systems, RTNS 2024 - Porto, Portugal Duration: 6 Nov 2024 → 8 Nov 2024 |
Publication series
| Name | RTNS 2024 - 2024 32nd International Conference on Real-Time Networks and Systems |
|---|
Conference
| Conference | 32nd International Conference on Real-Time Networks and Systems, RTNS 2024 |
|---|---|
| Country/Territory | Portugal |
| City | Porto |
| Period | 6/11/24 → 8/11/24 |
Keywords
- AUTOSAR
- Formal Specifications
- Dafny
- Predicate Transformers
ASJC Scopus subject areas
- Computer Networks and Communications
- Signal Processing
- Control and Systems Engineering
Fields of Expertise
- Information, Communication & Computing