Contribution: RailroadCrossing

The Railroad Crossing Example.

Authors:

  • Carlos Daniel Luna [Computing Science Department (InCo) at the Engineering School of the Universidad de la Republica, Montevideo, Uruguay. ]

Description:

This library present the specification and verification of one real time system: the Railroad Crossing Problem, which has been proposed as a benchmark for the comparison of real-time formalisms. We specify the system using timed automatas (timed graphs) with discrete time and we prove invariants, the system safety property and the NonZeno property, using the logics CTL and TCTL.

Keywords:

  • ctl
  • tctl
  • real time systems
  • timed automatas
  • safety
  • concurrency
  • properties
  • invariants
  • nonzeno
  • discrete time.

Source files: