Automated modular specification and verification of real-time reactive systems

Model-checking is a powerful automated technique for verifying finite state real-time safety critical systems, but suffers from a combinatorial explosion of states as system complexity increases. We introduce a method for compositional reasoning in real-time temporal logic that is suitable for model-checking finite state real-time reactive modules with data variables. This allows for the formal development of systems by top-down hierarchical program derivation. A system can be decomposed into modules, and the modules checked separately instead of checking the complete system all at once. This procedure often results in a significant decrease in the size of the reachability graphs that must be checked, particularly if the modules are loosely coupled. The compositional model-checking method developed in this paper is illustrated using a real time resource allocation problem and the StateTime toolset