May 3, 2010
FH Campus Wien
Vienna Institute of Safety & Systems Engineering
Favoritenstr. 226
1100 Vienna, Austria

This one-day seminar is organized by OSADL's Safety Critical Linux Working Group and will be held by OSADL's Safety Coordinator Prof. Nicholas Mc Guire. It will focus on tools for formal and semi-formal kernel and kernel module verification suitable for Free and Open Source software. The seminar is hosted by OSADL's Academic Member FH Campus Wien (University of Applied Sciences, Vienna Institute of Safety & Systems Engineering) in Vienna, Austria. Click here to display a map with directions.

Linux for safety-related systems has been in discussion since nearly a decade, i.e. since 2001 when the Health and Safety Information (HSE) report on SOUP for safety-related systems was published titled "Justifying the use of software of uncertain pedigree (SOUP) in safety-related applications" (HSE, 336/2001, PDF document). While this report did not exclusively focus on GNU/Linux - but it certainly was a main target, HSE published another assessment in 2002 that specifically dealt with GNU/Linux. The latter was titled "Preliminary assessment of Linux for safety related systems" (HSE RESEARCH REPORT 011, PDF document).

Nevertheless, with very few exceptions (FS20, SICAS ECC), there has been hardly any use of Linux in safety-related systems - one reason is that there are fundamental differences in how to approach pre-existing software compared to bespoke software. Making the necessary adaptations of the internal verification and certification procedures to cope with the specific requirements of Free and Open Source Software (FLOSS) and GNU/Linux is not an easy task and considered difficult and time-consuming. Overcoming this inertia is not a matter of a few simple methodologies being adopted but rather an introduction of a wide range of methods and procedures to allow achieving a comparable assurance in the correctness, reliability and robustness of FLOSS in general and GNU/Linux specifically. To this ends, the Safety Critical Linux Working Group is offering seminars on topics related to the utilization of GNU/Linux for safety-related systems.

The focus of this seminar is on verification tools suitable for FLOSS, i.e. static code analysis as well as using linear temporal logic (LTL) for liveliness and safety property modeling, i.e. using the Simple Promela Interpreter (SPIN), of concurrent processes and protocols. Roughly two third of bugs in the Linux kernel have been attributed to drivers, and within those bugs, a considerable amount can be detected by automated methods. Such methods are based on

• heuristic approaches derived from kernel developers experience,
• on formal methods like static code checking and on
• state-space exploration.

In the past years, a lot of progress has been made to automate these techniques and to scale them to a problem size suitable to tackle the Linux kernel. Current state-of-the-art FLOSS tools for software production can be used not only to enhance quality and ease maintenance but also to allow using FLOSS, notably GNU/Linux, in safety-related systems.

During the hands-on part of this seminar, we will run through different tools based on real-life kernel module examples. This will demonstrate how to use these tools to detect potential bugs and also to improve documentation, i.e. automatic generation of control flow diagrams and call graphs from source (user-space and kernel code).

The following FLOSS tools will be used:

• kernel build system - short intro to its QA capabilities
• sparse - semantic checking of kernel code
• lockdep - locking correctness validation in the kernel.
• stanse - static code analysis based on state-space exploration (user and kernel C-code)
• ddverify - SAT based device driver verification
• spin - model checking (primarily concurrency and protocol verification)
• ftrace - function graph tracing / sched latency statistics and friends
• gcov - kernel code coverage (kernel proper and modules)

The aim is to give participants a kick-start with respect to tooling that can support high availability and safety-related development in the context of GNU/Linux based systems and potentially help with certification demands. However, time constraints of this one-day session may prevent us to dig into the technological details of the individual methods - though reference material is, of course, provided.

Apparently, there are no hotels in walking distance of the FH Campus Vienna, but a couple of hotels are easily reachable via public transportation, please refer to this list.