Skip to Main content Skip to Navigation
Conference papers

A verifiable architecture for multi-task, multi-rate synchronous software

Abstract : Synchronous model-based software development techniques have proven to be both rigorous and efficient for the development of safety critical real-time software. Currently, the most common practice is to limit the use of synchronous techniques to single tasking or locally synchronous globally asynchronous multitasking scheduling schemes. This paper presents a technique for implementing multi-rate software on several tasks whilst preserving the determinism and verifiability of the synchronous approach. Our technique uses the synchronous framework in order to ensure rigour and verifiability, but implements different parts of a global synchronous model into separate tasks with a simple and efficient architecture. This architecture ensures determinism even in the presence of variations in execution time, and it also allows verification of the complete software by simulation or formal verification. This architecture has been applied to avionics software of a real aircraft’s equipment. Further perspectives are also provided.
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal-insu.archives-ouvertes.fr/insu-02270095
Contributor : Axelle Pagnier <>
Submitted on : Friday, August 23, 2019 - 6:11:46 PM
Last modification on : Thursday, June 11, 2020 - 5:04:09 PM
Long-term archiving on: : Friday, January 10, 2020 - 9:00:35 AM

File

ERTS2008_0038_paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : insu-02270095, version 1

Collections

Citation

Jean-Louis Camus, Pierre Vincent, Olivier Graff, Sebastien Poussard. A verifiable architecture for multi-task, multi-rate synchronous software. Embedded Real Time Software and Systems (ERTS2008), Jan 2008, toulouse, France. ⟨insu-02270095⟩

Share

Metrics

Record views

27

Files downloads

22