JUCS - Journal of Universal Computer Science 6(4): 460-473, doi: 10.3217/jucs-006-04-0460
Specifying and Verifying Real-Time Systems using Second-Order Algebraic Methods: A Case Study of the Railroad Crossing Controller
expand article infoL. J. Steggles
‡ Department of Computer Science, University of Newcastle, United Kingdom
Open Access
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.
real-time systems, algebraic specification methods, formal verification