https://www.dagstuhl.de/07241

June 10 – 15 , 2007, Dagstuhl Seminar 07241

Tools for the Model-based Development of Certifiable, Dependable Systems

Organizers

Michaela Huhn (TU Braunschweig, DE)
Hardi Hungar (OFFIS – Oldenburg, DE)
Doron A. Peled (Bar-Ilan University – Ramat Gan, IL)

For support, please contact

Dagstuhl Service Team

Documents

List of Participants
Case Study "Railway Level Crossing" [pdf]

Summary

The development of software for dependable systems on which the safety or security of individuals, organizations, and property may rely has become an important application and research field. In many cases, law enforces certification as a prerequisite for the introduction of a technical, dependable system. The certification formally assures that the systems and its development process meet the technical standards and all efforts have been made to reduce the risks. The complexity and discrete nature of software makes an assurance of the required properties of the software components of a dependable system extremely difficult. This applies even more as the software often constitutes the control in a so-called embedded system where coupling electronic and mechanical components is still a challenge. The relevant national and international standards recommend formal methods for the development of systems that shall be certified for the higher safety integrity levels. However, deriving constructive design guidelines and formally verifiable software constraints from safety requirements on the system level is still a challenging problem.

In many industries developing high-assurance products, model-based design is already well established and a number of tools used in safety-critical software design are founded on formal semantics and support in parts automated code generation, formal analysis, verification or error detection. But certification requires more than formal semantics of a modelling notation or the formal verification of the artefacts of a particular development step. Formal methods and tools have to be embedded in a seamless design process which covers all development phases and which includes an efficient construction of a safety case for the product. Moreover, whereas most (semi-)formal modelling approaches focus on functional issues additional concepts are required for dependable systems like fault tolerance, timing or security. Even if these concepts are addressed -- as several UML profiles do -- they are supported at most rudimentarily by the tools.

Conclusion

It was commonly agreed that formal specification has already reached the stage of being an effective support in the development of software-intensive dependable systems and that its role will increase in the future.

Technical progress in verification, for instance in component-oriented reasoning (assume-guarantee proofs) and (semi-)automated abstraction techniques, significantly expand the potential for applying formal methods on complex systems.

A tighter integration of models for design and models for verification has already begun and proven to be a key factor for the introduction of formal methods into the industrial practice. A number of verification approaches directly start with design models from UML or Matlab/Simulink as analysis input and offer seamless tool integration. However, these methods are often restricted to one particular verification goal that is considered relevant in one design phase or to a single concern like functional correctness or timing. Thus, a major challenge for the future will be to integrate formal approaches dealing with the different concerns that contribute to safety like functional correctness, reliability, timing, et cetera.

Classification

  • Semantics / Formal Methods
  • Verification / Logic Own Category: Dependable Systems

Keywords

  • Dependable systems
  • Safety
  • Security
  • Certification
  • Formal methods
  • Modelling
  • Verification
  • Tools

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.