Access Restriction

Author Ostroff, Jonathan S.
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Compositional Design ♦ Compositional Verification ♦ Deductive Tech-niques ♦ Reactive System Exhibit ♦ Internal Structure ♦ Combinatorial Explosion ♦ High-level Module ♦ Discrete Real-time System ♦ Compositional Reasoning ♦ Refinement Rule Guarantee ♦ Real-time System ♦ Structured Compositional Design Method ♦ Refinement Rule ♦ Quantitative Timing Constraint ♦ Statetime Toolset ♦ Large System ♦ Composition Rule ♦ Reactor Shutdown System ♦ Design Method ♦ Reactor Example ♦ Reactive System ♦ Discrete Realtime System
Description 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 compositional design method for discrete real-time systems that can be used to combat the combinatorial explosion of states in the verification of large systems. A composition rule describes how the correctness of the system can be determined from the correctness of its modules, without knowledge of their internal structure. The advantage of compositional verification is clear. Each module is both simpler and smaller than the system itself. Composition requires the use of both model-checking and deductive tech-niques. A refinement rule guarantees that specifications of high-level modules are preserved by 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 illus-trated using a reactor shutdown system that cannot be verified using the StateTime toolset (due to the combinatorial explosion of states) without compositional reasoning. The reactor example also illustrates the use of the refinement rule.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1999-01-01
Publisher Institution 71 [Pap94] [Per93] [Pet63] [Pet81