You are here: Home / Events, Seminars & Workshops / 
2024-11-12 - 23:20
OSADL Special Events

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

    Membership status

Access Fee

    Non-OSADL members

760 euros

    OSADL members

480 euros

Online Registration

To register online, please use this form.

Register Here!