Formal Methods and the Development of Dependable Systems.

Author: Jan Peleska

Abstract:
In this article we describe a formal framework for the development of dependable systems, supporting the systematic development of cooperating mechanisms designed to encounter combinations of threats. We focus on the combination of fault-tolerance mechanisms and security mechanisms in communication protocols. Until recently, fault-tolerant systems and secure systems were discussed and developed, at least in Germany, in different - often non-communicating - communities. Based on experiences with systems developed by the author in various industrial projects we motivate that a unified approach for the development of systems that combine both security and fault-tolerance properties will become increasingly important. Practical experience has shown that the a posteriori integration of security features into a fault-tolerant system and vice versa is much more complicated than pre-planning every desired dependability and security feature simultaneously during the specification phase of the project. Moreover, for maximum-quality systems intended to operate in safety-critical or otherwise sensitive environments the application of formal methods for the development and verification of the system is becoming increasingly `popular' and in some cases even mandatory. Therefore, we are investigating formal specification and verification techniques supporting the description of all dependability aspects. To be suitable for large-scale projects in an industrial development environment, a formal approach has to be supported by a development standard, providing a re-usable framework for the specification and verification activities to be performed during the various phases of system development. To this end, we will describe the application of our approach as embedded into the Vorgehensmodell (V-Model) which is authorized by the Germany Ministry of the Interior and considered as the state-of-the-art software development standard in Germany. Our approach will be illustrated by means of a case study describing a fault-tolerant and secure communication protocol.
Keywords: dependability - safety - reliability - availability - security - CSP - communication protocols

compressed poscript file (185KB)