Verification of the Properties of Asynchronous Real-Time Distributed Systems using the B-Formalism

Verification of industrial systems is becoming more challenging with the ever continuing advances in technology. Simulation was used, and still being used, but it cannot exhaustively examine all the execution scenarios of a given system. The alternative to simulation is formal methods that formally examine all the possible behaviors of a given system. However, formal methods suffer from the problem of explosion of the number of states; the number of states in practical system is often very large. A major contribution of this paper is that it suggests a modeling methodology that avoids the problem of explosion of the number of states, by reducing the number of system variables.