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)