Composition and refinement of discrete real-time systems

Reactive systems exhibit ongoing, possibly nonterminating, interaction with the environment. Real-time systems are reactive systems that must satisfy quantitative timing constraints. This paper presents a structured compositi onal design method for discrete real-time systems that can be used to comba t the combinatorial explosion of states in the verification of large system s. A composition rule describes how the correctness of the system can be de termined from the correctness of its modules, without knowledge of their in ternal structure. The advantage of compositional verification is clear. Eac h module is both simpler and smaller than the system itself. Composition re quires the use of both model-checking and deductive techniques. A refinemen t rule guarantees that specifications of high-level modules are preserved b y their implementations. The StateTime toolset is used to automate parts of compositional designs using a combination of model-checking and simulation . The design method is illustrated using a reactor shutdown system that can not be verified using the StateTime toolset (due to the combinatorial explo sion of states) without compositional reasoning. The reactor example also i llustrates the use of the refinement rule.