Verification of dynamic constraints for B event systems under fairness assumptions

Abstract

A B event systems is supposed to specify a closed system, i.e., the system is meant to be specified in isolation. So, the specification includes the specification of the system of interest and of its environment. Often, the environment supposes fairness constraints. Therefore, classically in a B system approach, we express the fairness of the environment by the specification of fair scheduler together with the events of the system of interest. This leads to an infinite state model even when the system is finite state by nature. This does not facilitate PLTL properties verification by model checking which is only effective on finite state models. In this paper, we propose to keep separate the fairness of the environment from the specification of the system of interest by a B event system. Then, the fairness is expressed as events which have to be fairly fired. So, a finite state system of interest has a finite state model. The chosen model is a finite labeled transition system which allows the model checking of PLTL properties using the fair events as assumptions. In the paper, we make diverse proposals-some of them are proposed as perspectives-for a verification under fairness assumptions. We use the protocol T=1 as a running example.