In: Proc. First Inf. Conf. on Integrated Formal Methods (IFM'99), 28029 June 1999, York, UK, pages 89-108. 1999.
Abstract: Reachability analysis has been one of the most successful methods for automated analysis of reactive and concurrent systems. It is based on an exhaustive enumeration of states and implemented in several verification tools. However, the major problem in applying this technique is the potential combinatorial explosion of the state space. To deal with this problem various reductions and symbolic techniques have been developed. This paper first presents an extension of the B language in order to express dynamic properties using logic formulas in LTL. After this, an approach to verification is presented which is performed on modules obtained by refinement rather than on the full specification. The number of states on which the verification is performed is then greatly reduced. Some patterns of properties are discussed and verified using the model checking on each module. BRP (bounded retransmission protocol) is given as an example.
Keywords: B language, linear temporal logic, model checking, modular verification, reactive systems.