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.