Test automation of safety-critical reactive systems

Abstract

This article focuses on test automation for safety-critical reactive systems. In the first part of the paper we introduce a methodology for specification, design and verification of fault-tolerant systems allowing to combine different methods in a systematic and consistent way, provided that these methods are compositional. The methodology indicates how to "switch" between formal verification and testing during the construction of (possibly large) reactive systems. We introduce the basic notions of testing as far as relevant in the context of reactive systems and relate them to the verification methodology. Part II formally describes our test automation method which is based on Hoare's CSP and takes Hennessy's testing theory as a starting point. It is indicated how this specific method fits into the general approach described in Part I. We introduce CSP test drivers which are trustworthy in the sense that they "approximate" refinement proofs, converging to a full proof with the increasing (possibly infinite) number of tests successfully executed. These drivers have been implemented in the VVT-RT (Verification, Validation and Test for Reactive Real-Time Systems) tool developed at Bremen University in cooperation with the University of Kiel, JP Software-Consulting and ELPRO LET GmbH. The presentation of this article is based on the lectures given by the first author during the WOFACS '96 workshop at the University of Cape Town.