The generalized railroad crossing: a case study in formal verification of real-time systems
- 1 January 1994
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 120-131
- https://doi.org/10.1109/real.1994.342724
Abstract
A new solution to the generalized railroad crossing problem, based on timed automata, invariants and simulation mappings, is presented and evaluated. The solution shows formally the correspondence between four system descriptions: an axiomatic specification, an operational specification, a discrete system implementation, and a system implementation that works with a continuous gate model.Keywords
This publication has 9 references indexed in Scilit:
- The generalized railroad crossing: a case study in formal verification of real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1994
- Larch: Languages and Tools for Formal SpecificationPublished by Springer Nature ,1993
- Verification of real-time systems using PVSPublished by Springer Nature ,1993
- The concurrency workbenchACM Transactions on Programming Languages and Systems, 1993
- Using mappings to prove timing propertiesDistributed Computing, 1992
- Forward and backward simulations for timing-based systemsPublished by Springer Nature ,1992
- A proof system for communicating shared resourcesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Safety analysis of timing properties in real-time systemsIEEE Transactions on Software Engineering, 1986
- Abstract requirements specification: A new approach and its applicationIEEE Transactions on Software Engineering, 1983