Hannover Messe 2024
COOL - Compact OSADL Online Lectures - April 2024 edition
HOT - Heidelberg OSADL Talks 2024 (online event)
OSADL Networking Day 2024 in Heidelberg, Germany
OSADL Special Events
OSADL Safety Critical Linux Working Group Seminar
Access fee - Registration - Map |
August 6 - 7, 2011
Beijing Shenzhou Aerospace Software Technology Co., Ltd.
#27 Yongfeng Road, Haidian District
Beijing 100094, China
Open Source for safety-related systems has been in discussion now for nearly a decade — the HSE report on SOUP for safety-related systems was published in 2001 (justifying the use of SOUP in safety-related applications, HSE 336/2001). Ever since the interest in using the plethora of Open Source in safety-related systems hqs grown.
Nevertheless with very few exceptions, there have been only limited deployments of Open Source in safety-related systems — one reason for this is that there are fundamental differences in how to approach pre-existing software compared to bespoke software and that the necessary adaptations in related industries have been slow.
Overcoming this inertia is not a matter of a few simple methodologies being adopted but rather an introduction of a wide range methods and procedures to allow achieving a comparable assurance in the correctness, reliability and robustness of FLOSS in general and of GNU/Linux specifically. To this end, the OSADL Safety Critical Linux Working Group is offering seminars on topics related to the utilization of Open Source and GNU/Linux for safety-related systems.
OSADL seminar: Introduction to Safety process and formal methods
The focus of this seminar is on basics of procedural safety, starting out from scratch. Thus, the seminar will address basics starting with terminology process foundations like requirements and design and relate it to the options of formal methods along the way. While the basics are a dry and partially boring topic, the afternoon of day #1 will cover less boring practical issues of using formal methods based on hands-on kickstarts into various available Open Source tools.
While the introduction of the theoretical background is "high-level", we intend to cover the foundations sufficiently to allow participants to dig deeper. The main intention of the hands-on part though is to show the practical capabilities of formal methods on complex existing software, notably on software as complex as the Linux kernel.
Some of the FLOSS tools that will be present (and used!) are:
- stanse - static code analysis based on state-space exploration (user and kernel C-code)
- spin - classic model checking (primarily concurrency and protocol verification)
- frama-c - framework for analysis and formal verification of code properties
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 Open Source based systems and potentially help with certification demands. It is not the intent of this two-day session to dig into the technological details of the individual methods/tools — though reference material will, of course, be provided.
Access Fee
| Access Fee |
| 760 euros |
| 480 euros |
Online Registration
To register online, please use this form.
