Specification Centered Testing
Verification and
Validation (V&V) of software for critical embedded control
systems often consumes up to 70% of the development resources.
Testing is one of the most frequently used V&V technique for
verifying such systems. Many regulatory agencies that certify
control systems for use require that the software be tested to
certain specified levels of coverage. Currently, developing test
cases to meet these requirements takes a major portion of the
resources. Automating this task would result in significant time and
cost savings. Our testing research is aimed at automating the
generation of such test cases. We propose an approach where we use a
formal model of the required software behavior (a formal
specification) for test-case generation and as an oracle to
determine if the implementation produced the correct output during
testing. This is what is referred to as Specification Centered
Testing. Specification centered testing offers several advantages to
traditional code based testing. The formal specification can be used
as the source artifact to generate functional tests for the final
product and since the test cases are produced at an earlier stage in
the software development, they are available before the
implementation is completed.
Central to our
approach is the use of model checkers as test case generation
engines. Model checking is a technique for exploring the reachable
state-space of a system model to verify properties of interest. When
a property violation is detected, a model-checker will produce a
counter-example as a witness, which is a sequence of states from the
initial system state to the violating state, where each state is an
assignment of values to system variables. Such a counter-example can
be viewed as a test case. For example, we can assert to the model
checker that a certain transition in a specification cannot be
taken. If this transition in fact can be taken, the model checker
will generate a sequence of inputs (with associated outputs) that
forces the model to take this transition – we have found a test
case that exercises this transition. One could systematically
generate such challenges to the model-checker based on some
user-defined levels of coverage of the software artifact and obtain
a set of test cases that achieves the desired coverage. There are
several research challenges that must be addressed to realize this
test generation approach.
Formalism and
criteria: We need a suitable formalism for expressing the
behavior of the software for critical control systems. It should
have enough structure in terms of which meaningful test criteria can
be expressed. It should also be general enough to capture various
software artifacts of interest, like requirement models and program
code.
Abstraction and
test data instantiation: To make model checking feasible one may
have to abstract away details. Software models pose serious
challenges since they typically include integer and real valued
variables leading to large or infinite state spaces. Abstraction
will give rise to test cases that have abstract data, which should
then be instantiated with concrete values.
Test data instantiation is achieved in the current testing framework
using concrete test data generators. Central to the use of these
test data generators is the translation from an abstract test case
(from NuSMV for instance) to a test specification language that
describes all the components of a test case—The Intermediate Trace
Representation (ITR). Figure shows the entire process of
translating an abstract test case derived from the model checker
NuSMV into a concrete test case in Java. In addition to the test
cases in Java, we also generate the test driver to execute these on
the implementation.
Figure 1: Concrete test data generation from
NuSMV counter examples.
Reducing test
set size: A straightforward generation of test cases will
inevitably lead to a large number of redundant test cases. For
example, a test case devised to test one specific transition in a
specification will also exercise many other transitions. One could
leverage this fact and develop techniques to eliminate redundant
tests.
Scalabilty and effectiveness: The usefulness of the
techniques and the test criteria must be empirically validated
through case studies and experiments. Of particular interest are the
scalability of these techniques to realistic models and the actual
coverage of the program code achieved by the generated test suites.
For the former, we conducted a comprehensive case study using six
models of progressively increasing complexity of the mode-logic in a
flight-guidance system, written in the RSML-e
language. We developed a framework for specification-based test
generation using the NuSMV model-checker and code based test case
generation using Java Pathfinder, and collected time and resource
usage data for generating test cases using symbolic, bounded, and
explicit state model-checking algorithms. The results seem to
indicate that a bounded model checker seems to be a suitable tool
for test case generation from formal specifications; it scales well
to systems of industrial relevance, it generates the shortest
possible test cases, and it is fully automated. There are, however,
some drawbacks. Most importantly, if the shortest test case needed
to cover a specific feature in the model is longer than the search
depth of the bounded model checker, we have no way of telling if the
test case simply does not exist or if it is longer than the search
depth.
|
