The generalized railroad crossing: a case study in formal verification of real-time systems

No abstract is available for this paper.

• Publication year

  1994

• Venue

  1994 Proceedings Real-Time Systems Symposium

• Publication date

  1994-11-01

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1109/REAL.1994.342724
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Forward and Backward Simulations, II: Timing-Based Systems

  1996cited by this paper
• On Communicating Sequential Processes

  1995cited by this paper
• The Concurrency Workbench : A Semantics Based Tool for theVeri cation of Concurrent Systems

  1994cited by this paper
• Simulation Techniques for Proving Properties of Real-Time Systems

  1993cited by this paper
• Larch: Languages and Tools for Formal Specification

  1993cited by this paper
• A Benchmark for Comparing Diierent Approaches for Specifying and Verifying Real-time Systems. In

  1993cited by this paper
• Verification of Real-Time Systems Using PVS

  1993cited by this paper
• A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems

  1993cited by this paper
• Time-Constrained Automata (Extended Abstract)

  1991cited by this paper
• A proof system for communicating shared resources

  1990cited by this paper
• Using mappings to prove timing properties

  1990cited by this paper
• Safety analysis of timing properties in real-time systems

  1986cited by this paper
• Abstract requirements specification: A new approach and its application

  1983cited by this paper

• A Survey on Formal Methods for Railway Interlockings: From Relays to Satellite-Based Moving Block Signaling

  2026cites this paper
• Hybrid I / 0 Automata *

  2023cites this paper
• Verification Method for Diagrammatic Workflow Specifications in Computer-Aided Design

  2022cites this paper
• Formal Methods in Railways: A Systematic Mapping Study

  2021cites this paper
• Timed Automata Benchmark Description

  2020cites this paper
• Automation of Workflow Design in an Industrial Enterprise

  2019cites this paper
• Clock Reduction in Timed Automata While Preserving Design Parameters

  2019cites this paper
• ATAC: A Tool for Automating Timed Automata Construction

  2019cites this paper
• Grammar-Algebraic Approach to Analyze Workflows

  2018cites this paper
• An investigation into Event-B methodologies and timing constraint modelling

  2017cites this paper
• Formal Verification of Train Control with Air Pressure Brakes

  2017cites this paper
• Development of timed RT-grammars for analysis of business process at manufacturing and in cyber-physical systems

  2017cites this paper
• Verification of critical systems described in real-time TiMo 

  2017cites this paper
• Calculus for decision systems

  2015cites this paper
• Timed Mobility and Timed Communication for Critical Systems

  2015cites this paper
• Towards a Unified Theory of Timed Automata

  2014influential citation
• The Power of Proofs: New Algorithms for Timed Automata Model Checking

  2014cites this paper
• A Logical Encoding of Timed $$\pi $$ -Calculus

  2013cites this paper
• Modeling and specification of distributed timed systems

  2013cites this paper
• Formal Specification of Railway Control Systems

  2013cites this paper
• Timed π-Calculus

  2013cites this paper
• Coinductive Constraint Logic Programming

  2012cites this paper
• STeC: A Location-Triggered Specification Language for Real-Time Systems

  2012cites this paper
• A One-Dimensional Sparse Space-Time Specification of the Generalized Railroad Crossing

  2012cites this paper
• Infinite Computation, Co-induction and Computational Logic

  2011cites this paper
• Patterns and model transformation tools for designing Contractual State Machines

  2011cites this paper
• Modeling conflicts resolution of Unmanned Aircraft System using a lightweight Duration Calculus

  2011cites this paper
• Modeling and verification of real-time and cyber-physical systems

  2011cites this paper
• An Extension of π-Calculus with Real-Time and its Realization in Logic Programming

  2011cites this paper
• Proving Safety Properties of the Steam Boiler Controller Formal Methods for Industrial Applications : A Case Study

  2010cites this paper
• Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R)

  2010cites this paper
• A monitoring approach to facilitate run-time verification of software in deeply embedded systems

  2010cites this paper
• Making real-time systems fault tolerant: a specification-based approach

  2010cites this paper
• Modeling and verification of stochastic hybrid systems using HIOA: a case study on DNA replication

  2010cites this paper
• Stochastic hybrid systems for DNA replication modeling

  2010cites this paper
• Timed Definite Clause Omega-Grammars

  2010cites this paper
• Logic Programming Foundations of Cyber-Physical Systems

  2010cites this paper
• We extend the concept of context-free grammars to timed context-free grammars and timed context-free ω-grammars. Informally, a timed context-free grammar

  2010cites this paper
• The Theory of Timed I/O Automata, Second Edition

  2010cites this paper
• Modelling and programming embedded controllers with timed automata and synchronous languages

  2009cites this paper
• Event order abstraction for parametric real-time system verification

  2008influential citation
• Event Order Abstraction for Parametric Timed Verification ∗

  2008cites this paper
• Validating Real Time Specifications using Real Time Event Queue Modeling

  2008cites this paper
• Decidable Veriication for Reducible Timed Automata Speciied in a First Order Logic with Time. Decidable Veriication for Reducible Timed Automata Speciied in a First Order Logic with Time

  2007cites this paper
• Translation Templates to Support Strategy Development in PVS

  2007cites this paper
• FMC-QE: A New Approach in Quantitative Modeling

  2007cites this paper
• Specification of Timed EFSM Fault Models in SDL

  2007cites this paper
• Rteq: modeling and validating infinite-state hard-real-time systems

  2007cites this paper
• Consistency of UML/SPT Models

  2007cites this paper
• Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic

  2007cites this paper
• Spatio-temporal Model Checking for Mobile Real-Time Systems

  2006cites this paper
• Specification and verification of mobile real-time systems

  2006cites this paper
• Verifying Average Dwell Time by Solving Optimization Problems

  2006cites this paper
• Coinductive Logic Programming

  2006cites this paper
• Time, abstraction and heuristics - automatic verification and planning of timed systems using abstraction and heuristics

  2006cites this paper
• pdfauthor Verifying Average Dwell Time of Hybrid Systems

  2006cites this paper
• Discrete Timed Automata

  2005cites this paper
• Use of synchronous concurrent algorithms in the development of safety related software

  2005cites this paper
• Executable hybridUML semantics: a transformation definition

  2005cites this paper
• INTEGRATED SPECIFICATION , VALIDATION AND VERIFICATION WITH HYBRIDUML AND OCL APPLIED TO THE BART CASE STUDY

  2004cites this paper
• A Logic Framework for Verification of Timed Algorithms

  2004cites this paper
• Formal verification of timed systems: a survey and perspective

  2004cites this paper
• Past pushdown timed automata and safety verification

  2004cites this paper
• Timed Patterns: TCOZ to Timed Automata

  2004cites this paper
• Stability of hybrid automata with average dwell time: an invariant approach

  2004cites this paper
• Lecture Notes on Hybrid Systems

  2004cites this paper
• Real Time Reactive Programming in Lucid Enriched with Contexts

  2004cites this paper
• Executable HybridUML and Its Application to Train Control Systems

  2004cites this paper
• Moby/DC - a tool for model-checking parametric real-time specifications

  2003cites this paper
• Timed I/O automata: a mathematical framework for modeling and analyzing real-time systems

  2003cites this paper
• Generalized discrete timed automata: decidable approximations for safety verificatio

  2003cites this paper
• Decidability of Invariant Validation for Paramaterized Systems

  2003cites this paper
• Modeling and verifying a Lego car using hybrid I/O automata

  2003cites this paper
• Presburger liveness verification of discrete timed automata

  2003cites this paper
• Constructing Test Automata from Graphical Real-Time Requirements

  2002cites this paper
• An inheritance-based technique for building simulation proofs incrementally

  2002cites this paper
• Decidable verification for reducible timed automata specified in a first order logic with time

  2002cites this paper
• Using BDDs with Combinations of Theories

  2002cites this paper
• Proving Correctness of the Basic TESLA Multicast Stream Authentication Protocol with TAME

  2002cites this paper
• Decidable Approximations on Generalized and Parameterized Discrete Timed Automata

  2001cites this paper
• TAME: Using PVS strategies for special-purpose theorem proving

  2001cites this paper
• Deductive verification of real-time systems using STeP

  2001cites this paper
• Past Pushdown Timed Automata

  2001cites this paper
• Analysis of three hybrid systems in timed µCRL

  2001cites this paper
• Classification schemes to aid in the analysis of real-time systems

  2000cites this paper
• Applying RT-Z to Develop Safety-Critical Systems

  2000cites this paper
• High-level modeling and analysis of the traffic alert and collision avoidance system (TCAS)

  2000cites this paper
• Deductive veri cation of real-time systems using STeP (

  2000cites this paper
• MODELLING THE GENERALIZED RAILWAY CROSSING WITH HYBRID ABSTRACT STATE MACHINES.

  2000cites this paper
• Simulating Aircraft Subsystems Using Non-Homogeneous Automata Networks

  2000cites this paper
• L . Sierra Comparing verification with HyTech , Kronos and Uppaal on the railroad crossing example Research Report LSV − 00 −

  2000cites this paper
• Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic

  2000cites this paper
• An inheritance-based technique for building simulation proofs incrementally

  2000cites this paper
• Automatic code generation for real-time reactive systems in TROMLAB environment

  2000cites this paper
• Specifying and Validating Train Control Systems Using an Appropriate Component-Based Petri Nets Model

  2000cites this paper
• Specifying and Verifying Real-Time Systems using Second-Order Algebraic Methods: A Case Study of the Railroad Crossing Controller

  2000cites this paper
• Abstraction from counters: an application on real-time systems

  2000influential citation
• Modeling and Verifying a Temperature Control System using Continuous Action Systems

  2000influential citation
• Completeness in formal specification language design for process-control systems

  2000cites this paper
• Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems

  2000cites this paper