Specifying and Verifying Real-Time Systems Using Second-Order Algebraic Methods:A Case Study of the Railroad Crossing Controller

摘要

Second-order algebraic methods provide a natural and expressive formal frameworkin which to develop correct computing systems. In this paper we consider using second-order algebraic methods to specify real-time systems and to verify their associated safety and utility properties. We provide a simple methodology for the design of correct real-time systems based on the notion of functional refinement. We demonstrate our ideas by presenting a detailed case study of the railroad crossing controller, a benchmark example in the real-time systems community. This case study demonstrates how real-time constraints can be modeled naturally using second-order algebras and illustrates the substantial expressive power of second-order equations.