package coq-railroad-crossing

  1. Overview
  2. No Docs
The Railroad Crossing Example

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. C
    Carlos Daniel Luna <http://www.fing.edu.uy/~cluna>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=aa5d5cef3b3a7a723b2040f90219f866

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.

Tags

keyword:CTL keyword:TCTL keyword:real time keyword:timed automatas keyword:safety keyword:concurrency properties keyword:invariants keyword:non-Zeno keyword:discrete time category:Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols date:February-March 2000

Published: 07 Jun 2016

Dependencies (2)

  1. coq >= "8.5" & < "8.6~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None