This one-day wo rkshop aims at gathering both academic and industrial users of the environ ments Frama-C and SPARK\, for sharing experiences and discussing perspecti ves.
\nIt is co-organized by CEA List (http://www-list.cea.fr/en/)\, Ad aCore (http://www.adacore.com/)\, In ria joint lab `ProofInUse' (http://www.spark-2014.org/proofinuse)\, and Université Paris-Diderot .
\nThis workshop will take place in t he context of the event `Open Source Innovation Spring 2017' (http://www.open-source-innovat ion-spring.org/) initiated by thematic group `Logiciel libre' of the c luster Systematic-Paris-Region and IRILL (`Initiative de Recherche et Inno vation sur le Logiciel Libre').
\n
Programme de la journée:
- \n
- Remov e Before Flight: Defect-Free Software and Agile Development in SPARK 2014\ , Martin Becker (TU München) \n
Development and verification of safety-critical software requires trained experts and takes its time. We challenged this opinion by developing an en tire flight stack for a high-altitude glider in Ada/SPARK 2014 within only a few months of time. We started implementation with an initial software design and continuously applied static analysis to eliminate defects\, ada pt the design to verification needs\, and to ensure a goal-oriented progre ss during the implementation phase. This talk introduces the project\, exp lains the workflow that has been established\, and reflects on project pro gress\, final results and remaining challenges of verifying SPARK programs .
\n- \n
- Static vs runtime checking i n Frama-C/SPARK\, Claude Marché (Inria) \n
- CubedOS: A Verified CubeSat Operating System\, Carl Bran don\, Peter Chapin (Vermont Technical College) \n
- \n
- Struc turing an Abstract Interpreter through State and Value Abstractions\, David Bühler (CEA List) \n
The new a bstract interpreter of Frama-C\, EVA\, enjoys a modular and extensible arc hitecture\, where new analysis domains may be plugged-in. These domains ca n interact through different means to achieve maximal precision. First\, t hey work cooperatively to emit the alarms that exclude the undefined behav iors of the program. Second\, they exchange information through abstractio ns of the possible values of expressions. Those value abstractions are the mselves extensible\, should two domains require a novel form of cooperatio n. In this talk\, we present this communication system and illustrate how the different domains of EVA benefit from it.
\n- \n
- Specifying and proving correctness of Linux kernel compone nts with ACSL\, Alexey Khoroshilov\, Mikhail Mandrykin (Linux Verification Center\, ISPRAS) \n
The talk pre sents our experience in deductive verification of Linux kernel components using Frama-C with AstraVer plugin (a fork of Jessie). It includes an over view of new features that were required to verify kernel code and a discus sion of possible improvements in ACSL specification. Particularly\, ACSL s uggests unbounded semantics for operations on integral numbers in specific ations and also does not provide special constructs for specifying relativ ely complex proofs\, e.g. inductive proofs through lemma functions. Our ex perience has shown benefits of using different integer semantics and lemma functions\, in particular for fragments involving complicated bit-twiddli ng tricks used for bit-counting\, checksum computation\, byte reorderings etc.
\n- \n
- Development of security-c ritical software with SPARK/Ada at secunet\, Stefan Berghof er (secunet) \n
In this talk\, we describe how t he SPARK/Ada language and toolset is used for the development of component -based high-security systems at secunet Security Networks AG. To make the complexity of assessing the security of these systems manageable\, the com ponents are running on top of the Muen separation kernel\, which ensures t hat they can only communicate with each other via designated channels. We give an overview of our methodology for verifying trusted components using a combination of the SPARK tools and the interactive proof assistant Isab elle\, which is used for solving proof obligations that are beyond reach o f automatic provers. We illustrate the methodology using selected correctn ess properties of a cryptographic library.
\n- \n
- 09:00 -
From learning examples to high-integrity middleware\, comparing ACSL and SPARK\, Christophe Garion\, Jérôme Hu ghes (ISAE) \n
In this talk\, we report on two e xperiments 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-integr ity restrictions). As part of the TASTE and ESROCOS projects\, we want to demonstrate absence of runtime errors. The two runtimes share common algor ithms\, but leverage different constructs (pointers\, OS APIs vs native la nguage constructs). We report on the current status of both activities\, a nd required blocks to complete this task.
\n- \n
- Real Behav ior of Floating Point Numbers\, François Bobot (CEA List) \n
Floating point numbers are p ervasively used in programs\, yet when one starts to look into them it bec omes clear that they are nothing like reals. There are a lot of counter-ex amples of simple real number properties that are completely wrong for floa ting point numbers. Yet\, actual C or SPARK developers are using floating point numbers and expect their code to behave like reals! and in many case s they are indeed right. However it is difficult for state-of-the-art prog ram verification tools to prove that the floating point properties they ar e using are true. We will show the result of the fruitful collaboration do ne in the SOPRANO project that allowed the Frama-C and SPARK tools to tack le these problems orders of magnitude faster than before.
\n\n