OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

From learning examples to High-Integrity Middleware, comparing ACSL and SPARK

Garion, Christophe and Hugues, Jérôme From learning examples to High-Integrity Middleware, comparing ACSL and SPARK. (2017) In: Frama-C & SPARK Day 2017, 30 May 2017 (Paris, France). (Unpublished)

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


In this talk, we report on two experiments using ACSL and SPARK. In the first part, we introduce SPARK-by-Example, a SPARK translation of the well-known ACSL-by-Example booklet. This work has been started to learn more about the SPARK2014 language. In the second part, we report on an ongoing effort to port an AADL runtime, a middleware meant for safety-critical systems. ISAE has implemented two variants of this runtime: one targeting typical C/RTOS (FreeRTOS, RTEMS, RT-POSIX), and one targeting Ada 2005 (Ravenscar profile and high-integrity restrictions). As part of the TASTE and ESROCOS projects, we want to demonstrate absence of runtime errors. The two runtimes share common algorithms, but leverage different constructs (pointers, OS APIs vs native language constructs). We report on the current status of both activities, and required blocks to complete this task.

Item Type:Other Conference
Audience (conference):National conference without published proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Laboratory name:
Deposited On:11 Jul 2017 14:53

Repository Staff Only: item control page