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.