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. H
    Hugo.Herbelin@inria.fr

Sources

v8.8.0.tar.gz
md5=b3d43148c290b04b040e11078b4acf26

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: 06 Feb 2019

Dependencies (2)

  1. coq >= "8.8" & < "8.9~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None