Test Automation of Safety-Critical Reactive Systems.
Authors: Jan Peleska and Michael Siegel
This article focuses
on test automation for safety-critical
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.
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 Capetown.
Keywords: Test generation, test strategies, dependability,
fault-tolerance, reactive systems