Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)
Sept. 7, 2005 to Sept. 9, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.52
Mark Trakhtenbrot , Holon Academic Institute of Technology, Israel
<p>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.</p> <p>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 Statemate 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.</p> <p>A realistic Rail Cross Control example is used to illustrate the approach.</p>
M. Trakhtenbrot, "Use of Verification for Testing and Debugging of Complex Reactive Systems," Third IEEE International Conference on Software Engineering and Formal Methods(SEFM), Koblenz, 2005, pp. 13-22.