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

Abstraction and Composition of Discrete Real-Time Systems

Jonathan Ostroff

Technical Report CS-ETR-95-02

York University

September 15, 1995


This paper extends the TTM/RTTL deductive and model-checking framework for real-time reactive systems with a structured design method using the notions of real-time reactive modules, module abstrac-tion and module composition. Equivalence transformations are used to obtain abstract systems, and a composition theorem is provided for deduc-ing global properties from module specifications. The StateTime tool is used for checking module correctness. Abstraction and composition are applied to an actual industrial example involving the delay reactor trip for a nuclear reactor consisting of three independent microprocessors based con-trollers. Timing, concurrency, integer data, communication and nondeter-minism are all important elements of the problem. While the StateTime tool can verify a single microprocessor controller (under 100k states and edges), the complete 3-version system suffers from a combinatorial explo-sion of states. By contrast, the proposed design method is able to verify the example, and scales up to larger systems.

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.