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.10.0.tar.gz
md5=6b070cfc66b79c57cdbd3d4ed55a0ee4

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 Dec 2019

Dependencies (2)

  1. coq >= "8.10" & < "8.11~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None