next up previous

Final Report of the COST-247 Action

Reachable state space analysis of LOTOS specifications

Alain Kerbrat

Centre Equation
2, avenue de Vignate
F-38610 Gieres
tel : +(33) 4 76 63 48 48
fax : +(33) 4 76 63 48 50


We present a symbolic analysis technique for LOTOS programs with integer variables on which only linear expressions are allowed. The technique is applicable to models generated by the CAESAR compiler which are Petri nets extended with guarded commands. It allows to compute a predicate on variables characterizing the set of the reachable states or an upper approximation of it. Predicates are represented as systems of linear inequalities on program variables. We implemented a tool for performing the operations necessary for the analysis such as conjunction, disjunction, widening operation as well as comparison of predicates. The method is applied to two examples showing that non trivial relations between program variables can be discovered.

This presentation has been given during the COST-247 3rd Management Committee Meeting (Evry, France, September 19--20, 1994).

COST-247 Working Group(s): 1-2

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page