Model-Checking in Simulations of Distributed Systes.

Formal verification techniques are promising tools to deal with the problems associated with the design of concurrent systems. However, they are often hard to use and the state-space explosion problem makes that they are not applicable to large size systems. Some techniques exist to allow the use of these methods on larger systems at the cost of giving up the guarantee that errors will be detected. This paper describes a technique and its application which allows a form of temporal logic model checking that does not require states of the system to be stored in memory. This makes it possible to integrate model-checking into a discrete-event simulator for complex distributed real-time systems. It is shown how so-called safety properties expressed in linear temporal logic can be monitored during a forward simulation of the system.