Reasoning About the Reliability of Multi-version, Diverse Real-Time Systems

This paper is concerned with the development of reliable real-time systems for use in high integrity applications. It advocates the use of diverse replicated channels, but does not require the dependencies between the channels to be evaluated. Rather it develops and extends the approach of Little wood and Rush by (for general systems) by investigating a two channel system in which one channel, A, is produced to a high level of reliability (i.e. has a very low failure rate), while the other, B, employs various forms of static analysis to sustain an argument that it is perfect (i.e. it will never miss a deadline). The first channel is fully functional, the second contains a more restricted computational model and contains only the critical computations. Potential dependencies between the channels (and their verification) are evaluated in terms of aleatory and epistemic uncertainty. At the aleatory level the events ''A fails" and ''B is imperfect" are independent. Moreover, unlike the general case, independence at the epistemic level is also proposed for common forms of implementation and analysis for real-time systems and their temporal requirements (deadlines). As a result, a systematic approach is advocated that can be applied in a real engineering context to produce highly reliable real-time systems, and to support numerical claims about the level of reliability achieved.

I. Introduction

For high-integrity real-time systems, it is imperative that all system deadlines are met on all occasions. A general approach to improve reliability in systems is to introduce redundant components. However, replication will not be effective if the sources of unreliability are defects in the way the system has been analysed, rather than in the implementation of the system. In this paper we investigate the properties of a dual channel system in which diverse forms of analysis (as well as diverse implementations) are explored. The paper follows the model introduced by Littlewood and Rushby [24] for general system reliability. A two-channel system is employed. The first channel (Channel A) is fully functional with its temporal behaviour being validated by a measurement-based approach. The other channel (Channel B) only implements the crucial software components, has a restricted software architecture and is validated by static analysis.