Reachable State Space Analysis of LOTOS programs

Alain Kerbrat

Proceedings of the 7th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols FORTE'94 (Bern, Switzerland), October 1994

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 Lotos compiler of the Caesar-Aldebaran toolbox 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.

16 pages

PDF

PostScript