Workshop: C Program Quality Assurance using ACSL

Using unit-tests for quality assurance becomes disproportionately more expensive with rising safety levels. While formal verification has been floating around in academic communities, it recently has found entrance to industrial practice. Companies in the field of aeronautic high-integrity embedded systems are known to use verification as a more efficient alternative to unit-testing that none the less achieves a maximal safety level. The next version of the avionics software standard DO-178-C, expected in late 2010, makes it possible to replace parts of traditional software tests by formal verification methods. This can help to reduce validation costs and to produce a higher assurance than testing.
The ANSI/ISO-C Specification Language ACSL has been particularly designed to meet verification needs on an industrial level. ACSL is used in the Frama-C analysis tool from CEA LIST. Fraunhofer FIRST is evaluating Frama-C in an industrial case study and is one of the few experts able to adapt the tool to the needs of different industries. The institute supports its customers in integrating Frama-C in their existing software development processes.

From October 21st-22nd 2010, Fraunhofer FIRST and CEA LIST will offer an introductory study-course in ACSL which takes place at Fraunhofer FIRST, Berlin-Adlershof.

The workshop is expressly aimed at experienced C programmers who are novices in the area of formal verification. The course will consist of lectures combined with exercises in Frama-C. There will also be several opportunities for plenary discussions.

Participants shall supply their own note-books to perform the exercises. Having Frama-C pre-installed on it is possible but not mandatory. A Live CD will be provided and is included in the symbolic course fee of € 100 .

Installation CD-ROMs can also be considered if they are requested not later than October 8th 2010.

Schedule

Thursday October 21st, 2010
9:45 Welcome: Prof. Dr. Holger Schlingloff (Fraunhofer FIRST)
10:00 General Introduction: Dr. Jens Gerlach (Fraunhofer FIRST)
Experience Report: "Formal Verification in Aeronautics: Current Practise and Upcoming Standard": Yannick Moy (Adacore)
11:00 Introduction to ACSL and its GUI: PhD Virgile Prevosto (CEA LIST)
12:30 Lunch
14:00 Basic ACSL features, Exercise: simple-loop program inspecting an array: Dr. Jochen Burghardt (Fraunhofer FIRST)
15.45 Coffee break
16:15 Advanced ACSL features, Predicate definitions, Exercise: simple-loop program modifying an array: PhD Pascal Cuoq (CEA LIST)
17:45 Discussion
18:15 Conclusion of first day

Friday October 22nd, 2010
9:00 Short presentation of Value Analysis and its use of ACSL: PhD Pascal Cuop (CEA LIST)
10:00 Deductive verification of data structures: Dr. Jens Gerlach (Fraunhofer FIRST)
11:00 Coffee break
11:15 Deductive verification of data structures: Dr. Jens Gerlach (Fraunhofer FIRST)
12:30 Lunch
14:00 Tips and tricks in verification: PhD Virgile Prevosto (CEA LIST)
15:45 Discussion
16:15 Conclusion of Workshop

Please register yourself until October 8th 2010 on our website.