Testing and formal verification of behavioral models

A key issue in model checking is how to locate faults that caused property violation, when a lengthy counterexample is returned. Our work has addressed this issue in the framework of Scade or Simulink design models [BVWW10]. The approach is based on a structural analysis that identifies paths of the model that are activated by a counterexample over time. This analysis allows the extraction of relevant information to explain the observed violation. It may also serve to guide the model checker toward the search for different counterexamples, exhibiting new path activation patterns and thus new ways to violate the property. The aim is to give engineers as much usable feedback as possible before a fix is attempted. The approach has been implemented in a tool called STANCE (Structural ANalysis of CounterExamples). It is closely related to path-based analysis techniques developed for structural testing. Current work further elaborates on the approach, as regards both the extraction of explanatory information (for paths traversing of numerical operators) and the comparison of strategies for obtaining new counterexamples (path-based strategies combining symbolic and heuristic techniques).

Publications

[BVWW10] T. Bochot, P.Virelizier, H. Waeselynck, V.Wiels: Paths to property violation: a structural approach for analyzing counter-examples, Proc. 12th IEEE Int. High Assurance Systems Engineering Symposium (HASE 2010), San José (USA), November 2010, pp.74-83. 

Back to TSF Research Topics page