Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Counterexample-Based Error Localization of Behavior Models
verfasst von : Tsutomu Kumazawa, Tetsuo Tamai
Erschienen in: NASA Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Behavior models are often used to describe behaviors of the system-to-be during requirements analysis or design phases. The correctness of the specified model can be formally verified by model checking techniques. Model checkers provide counterexamples if the model does not satisfy the given property. However, the tasks to analyze counterexamples and identify the model errors require manual labor because counterexamples do not directly indicate where and why the errors exist, and when liveness properties are checked, counterexamples have infinite trace length, which makes it harder to automate the analysis. In this paper, we propose a novel automated approach to find errors in a behavior model using an infinite counterexample. We find similar witnesses to the counterexample then compare them to elicit errors. Our approach reduces the problem to a single-source shortest path search problem on directed graphs and is applicable to liveness properties.