392205 System Safety und Security II (V) (SoSe 2014)

Ultrareliable Software Programming with SPARK.

SPARK is a system consisting of executable imperative program code, a sublanguage of the language Ada, with a collection of tools which check exact properties of the executable code and its associated variable and data-structure declarations. The tools can be and should be used as the program code is being written, in order to rule out coding errors at the very time they might occur. This programming paradigm is known as "Correct-by-Construction", or CbC, programming. The SPARK toolset is built and maintained by the British company Altran-Praxis, and the environment in which it may be used, the GNU Ada Toolkit (GNAT) environment, which includes an Ada compiler for the resulting code, by the US company AdaCore. We use a GPL-licensed version. We also use tutorial material developed for use in industrial programming courses by Altran-Praxis.

Students in this course will learn to program in Ada as well as the use of the SPARK toolset to construct and check programs for desired properties rigorously. It is assumed that students know and can program in at least one imperative programming language such as C, Java or Pascal.

The tools include a data-flow checker, an information-flow checker and a pre-/postcondition theorem prover. The first two are algorithmic and fully automatic. The third must be "steered" by the programmer towards the goal. Unlike many programming languages such as C and Java, the sublanguage of Ada which SPARK executes is unambiguous; all programs written in SPARK have deterministic flow of control and deterministic behavior, which makes it especially suitable for the precise analysis required in developing safety-critical programs.

Software developed using these CbC techniques has shown itself to be considerably more error-free than critical software developed using other "standard" methods (deployed recent SPARK code has error rates of 1 in 25,000 lines of executable code (LOC); industry rumor says that "usual" methods result in error rates of about 1 in 1,000 LOC).

Programmers able to work with ultrareliability techniques such as CbC are increasingly in demand in industry. Digital systems are increasingly to be found in large engineered systems, and often take over safety-critical or security-critical roles. The suppliers of such software have a legal responsibility to ensure that the software is fit-for-purpose, and using CbC development methods helps discharge the responsibility to ensure that the software fulfils its specification.

The lecture, exercise session, and laboratory should be taken in the same semester, and count together for 5 credit points (LP). The points may be applied in the module System Safety and Security.

Requirements for participation, required level

Mathematik I, Einführung in die Informatik oder Algorithmen und Datenstrukturen
Nützlich: Theoretische Informatik