Observation Graph implementation for TINA toolbox

Rodrigo Tacla Saad (1) , François Vernadat (1) , Bernard Berthomieu (1) , Silvano Dal Zilio (1)

1 LAAS-OLC

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.

Domaines: Génie logiciel [cs.SE]

Rodrigo Tacla Saad, François Vernadat, Bernard Berthomieu, Silvano Dal Zilio. Observation Graph implementation for TINA toolbox. 12th European Workshop on Dependable Computing, EWDC 2009, May 2009, Toulouse, France. 4 p. ⟨hal-00380671⟩