Use of verification for testing and debugging of complex reactive systems

Safety-critical reactive systems are characterized by a complex behavior, making their testing and debugging a very difficult task. Observed incorrect behavior might be hard to reproduce: even small changes in order or in time at which input events occur may have a significant impact on system reaction. The challenge is how to utilize (typically, partial) information about failed system run to reproduce and localize the problem. For statechart-based models of reactive systems, it is shown how testing and model checking can be combined to reproduce errors observed during execution of code generated from model. This approach is based on the use of State mate ModelChecker tool. The main idea is to use the available knowledge about "irreproducible" run that violates system property P, in order to properly set up verification for reachability of not P. A realistic rail cross control example is used to illustrate the approach.