High Integrity Programmable Electronic Systems

Motivation

Software is increasingly being used in safety-critical applications where failure could cause loss of human life, personal injury, or significant material damage. High integrity programmable systems denote a class of software controled applications that are characterized by a sensible interplay of heterogeneous technologies (software and various forms of hardware), high requirements on the dependability of all system components, including the safety, security, adequacy and correctness of the embedded software, and – depending on national regulations – the need to undergo extensive certification procedures. Examples of high integrity applications occur in process control (e.g., in chemical industry or nuclear power generation), traffic control, or in medical systems.

High integrity programmable electronic systems for safety critical control and regulation applications form a new field that stands at the very beginning of its treatment in research, development, and teaching. The significance of this subject arises from a growing awareness for safety in our society, on the one hand, and from the technological trend towards more flexible, i.e., program controlled, technical devices, on the other hand. A major objective is to reach the state that such systems can be constructed with a sufficient degree of confidence in their dependability that enables their licensing for safety critical control and regulation tasks by the pertaining authorities on the basis of formal approvals. But authorities are currently still very reluctant in approving safety related systems whose behaviour is exclusively program controled, leading to the unsatisfactory situation that safety licensing, in general, is still denied for highly safety critical systems relying on software with non-trivial complexity. The reasons lie mainly in a lack of confidence in complex software systems and in the high effort needed for their safety validation following current practices. Although formal specification and verification techniques are increasingly accepted as an important approach to achieve high integrity software, their use in practice is still limited due to the lack of effective tools and the need for special expertise.

In this context, the seminar aimed at the evaluation and comparison, of existing, more or less, formal methods with respect to their use in practice and indicating directions for future development. The seminar thereby spanned several dimensions of computer and computing science including safety and fault tolerance strategies, formal methods, languages with high integrity features, human factors in risk reduction and program understanding, software verification, safety-oriented software architectures and operating system kernels, and hardware correctness. These dimensions were supplemented with application experiences of licensing authorities and were confronted with particular requirements and characteristics of the application domain such as fuzzy-ness, distribution, or predictability and timeliness of behaviour.