coq-railroad-crossing

The Railroad Crossing Example. 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.

opam install coq-railroad-crossing.8.5.0
homepage
https://github.com/coq-contribs/railroad-crossing
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/railroad-crossing/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/railroad-crossing/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-railroad-crossing/coq-railroad-crossing.8.5.0