Specifying and Verifying Real-Time Systems using Second-Order Algebraic Methods: A Case Study of the Railroad Crossing Controller
L. Jason Steggles · Zenodo (CERN European Organization for Nuclear Research) · 2020
Abstract: Second{order algebraic methods provide a natural and expressive formal framework in 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 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 modelled naturally using second{order algebras and illustrates the substantial expressive power of second{order equations.