Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
1998 Technical Reports

Composition and Refinement of Discrete Real-Time Systems

Jonathan S. Ostroff

Technical Report CS-1998-10

York University

November 25, 1998

Abstract

Reactive systems exhibit ongoing, possibly non-terminating, 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 techniques. 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 illustrated using a reactor shutdown system that can-not 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 refine-ment rule.

This paper will appear in the ACM Trans. on Software Engineering in 1999. For details of copyright, see http://www.acm.org/pubs/copyright.policy. This document has been provided by the author as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders (ACM), notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Download paper in PDF format.



The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.