Observation Graph implementation for TINA toolbox

Abstract

Model Checking is a formal technique for the verification of finite systems. However, it is well known that this technique suffers from the state explosion problem. We describe work in progress to implement in the TINA toolbox an enumerative variant of a state based observation graph algorithm defined by Klai and Poitrenaud.

Publication
In EWDC 200912th European Workshop on Dependable Computing