Personal tools

fast

Fault Model-Based Test Generation from Text-Based Specifications

Research Topics

  • Model-Based Systems

Project Details

Passenger vehicles turn more and more into electronic platforms, and the application of embedded systems already affects safety critical areas. With the increase of the number of functions in cars, electronic systems have become more and more complex. In current practice, requirements are normally not specified and realized in a formal way. This is unlikely to change in the near future and prevents the application of formal verification methods. To ensure correctness of the systems to a certain degree despite this fact, testing of embedded systems is still necessary and crucial.

This work presents the main results of a project conducted with the support of Audi AG. FAST (Fault-model And Specification-based Test Generation) is a system for the automated generation of test suites based on functional requirements and has been developed with the goal that it can be easily integrated into the current work process at Audi AG. To realize this, not only the computation of tests has to be solved, but also an appropriate interaction with the user, including support for formulation of requirements and export of the results to a standard tool for further processing, becomes a major challenge.

For modeling the functional requirements, a Formal Requirement Language (FRL) is introduced. Each requirement is described as an implication in a real-time interval temporal logic. The formalization of the intuitions behind existing man-made test cases leads to a set of fault operators mutating the original functional requirement specification (in FRL) and, thus, generating fault models.

The approach uses model-based test generation to compute definitely discriminating tests (DDTs) where the test input guarantees the observability of distinctions between ok-models (requirements) and fault models. In contrast, approaches based on counterexample generation through model checking cannot guarantee this.

The functional requirements are translated from FRL into timed constraint automata representing the language for test generation. In order to tame state explosion, requirements that are irrelevant for an individual test task are ignored, and thus only a partial model rather than the entire set of requirements is used for computation. Several plausible subclasses of the complete set of DDTs are defined in order to reduce the search space. The test generation algorithm computes tests incrementally with regard to the number of input intervals. It is realized by performing a search in the state-space of the timed automata.

The correctness of the translation of FRL into timed constraint automata and of the test generation algorithm (along with its completeness) is formally proven. In addition, a proof is given for the completeness of test generation based on the partial models.

In order to ease integration into the current work processes, FAST comprises appropriate front-ends regarding both input and output: Since it is unrealistic to expect the engineer to formulate requirements in a formal language like FRL, a natural language approach based on sentence templates was developed and the generated tests can be automatically exported to EXAM, a tool for the automatic execution of a test suite on a test bench used in the automotive sector.

FAST is being applied and evaluated on a real-world case-study capturing parts of the adaptive cruise control (ACC).

Media

There are currently no items in this folder.


Document Actions