Abstract:

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.