Model-based Test Generation


The goal of this project is to generate tests that can be used to validate an implementation confirms to a specification. There are two approaches that we are pursuing: one is automatic test generation from models written in EFSM (Extend Finite State Machine) or hybrid systems, and another is manual test generation from RTSJ (Real-Time Specification of Java). For the latter, visit Test Suite for Realtime Java (created in 2001).

For the model-based test generation, the goal is to automatically generate a test suite that meets particular coverage criteria from specification in EFSM or hybrid systems. The approach to integrate random test-trace generator with targeted test-trace generator based on model checking. We use model-checking approaches to make test generation more flexible, efficient, and effective. An enhanced model checker will work as a generic test generator: it takes the coverage criteria encoded in some temporal logic and the specification system as the input, and produces the test suite achieving the coverage.  Essentially the combination of the generic test generator and the criteria given as temporal properties will function as a special test generator dedicated for such criteria. This is done without having to implement a different test generator for each coverage criteria. The approach also exploits well-developed model-checking techniques to make test generation more efficient. Moreover, the richness of temporal properties allows us to express both generic and system-specific coverage criteria.

The following figure described the overall approach to the test generation from hybrid system models specified in CHARON.


People

External Collaborators

Former Members

Activities

On the theoretical side, we have shown that many traditional coverage criteria can be encoded as w-CTL formulas [HLO02]. On the practical side, we are implementing a preliminary version of randomized test generator for CHARON. Our next step is to implement a counter-example guided test generator for CHARON.

Publication

Links

Meetings