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

Author(s): Steggles LJ

    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 provide a simple methodology for the design of correct real-time systems based on a simple 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 modelled naturally using second--order algebras and illustrates the substantial expressive power of second--order equations.

      • Date: July 2000
      • Series Title: Department of Computing Science Technical Report Series
      • Pages: 15
      • Institution: Department of Computing Science, University of Newcastle upon Tyne
      • Publication type: Report
      • Bibliographic status: Published

      Keywords: real-time, algebraic specification, second-order algebra, formal verification, formal verification, algebraic specification case study

      Staff

      Dr Jason Steggles
      Senior Lecturer