A Compositional Proof of a Real-Time Mutual Exclusion Protocol

In this paper, we apply a compositional proof technique to an automatic verification of the correctness of Fischer's mutual exclusion protocol. It is demonstrated that the technique may avoid the stateexplosion problem. Our compositional technique has recently been implemented in a tool CMC 5, which verifies the protocol for 50 processes within 172.3 seconds and using only 32MB main memory. In contrast all existing verification tools for timed systems will suffer from the stateexplosion problem, and no tool has to our knowledge succeeded in verifying the protocol for more than 11 processes.

• Publication year

  1996

• Venue

  Theory and Practice of Software Development

• Publication date

  1996-06-25

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/BFb0030626
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Compositional model-checking for real-time systems

  1998influential reference
• Hypergraph Optimization Problems: Why is the Objective Function Linear?

  1996cited by this paper
• UPPAAL in 1995

  1996cited by this paper
• Theory and Practice of Action Semantics

  1996cited by this paper
• Partial Orders and Verification of Real-Time systems

  1996cited by this paper
• The symbolic model-checking for real-time systems

  1996cited by this paper
• Combining Algebraic and Set-Theoretic Specifications (Extended Version)

  1996cited by this paper
• Pushdown Processes: Games and Model-Checking

  1996cited by this paper
• Diagnostic Model-Checking for Real-Time Systems

  1995cited by this paper
• From Timed Automata to Logic - and Back

  1995cited by this paper
• Automated Analysis of an Audio Control Protocol

  1995cited by this paper
• Compositional and symbolic model-checking of real-time systems

  1995influential reference
• Partial model checking

  1995influential reference
• Automatic Veri(cid:12)cation of Real{Time Communicating Systems by Constraint{Solving (cid:3)

  1994influential reference
• Verifying ET-LOTOS programmes with KRONOS

  1994cited by this paper
• Automatic verification of real-time communicating systems by constraint-solving

  1994cited by this paper
• A Theory of Timed Automata

  1994cited by this paper
• Symmetry and model checking

  1993cited by this paper
• Higher-Order Algebra, Logic, and Term Rewriting

  1993cited by this paper
• Exploiting symmetry in temporal logic model checking

  1993cited by this paper
• Model checking and abstraction

  1992cited by this paper
• A partial approach to model checking

  1991cited by this paper
• Symbolic Model Checking: 10^20 States and Beyond

  1990cited by this paper
• A stubborn attack on state explosion

  1990cited by this paper
• Symbolic model checking: 1020 states and beyond

  1989cited by this paper

• Robustness in real-time systems

  2011cites this paper
• Compositional and Quantitative Model Checking (Extended Abstract)

  2009cites this paper
• Contrôle et implémentation des systèmes temporisés

  2007influential citation
• Validation and Veriication of Real Time Systems

  2007cites this paper
• E cient Memory DeallocationTechniques in Real-Time Model-CheckingFredrik

  2007cites this paper
• Tool supported real-time system verification with combination of abstraction/deduction and model checking. (Abstractions booléennes pour la vérification des systèmes temps-réel)

  2007influential citation
• Quotient-based control synthesis for partially observed non-deterministic plants with mu-calculus specifications

  2007cites this paper
• Predicate diagrams for the verification of real-time systems

  2007cites this paper
• Verifying Networks of Timed Processes

  2006cites this paper
• Properties as Processes: Their Specification and Verification

  2005cites this paper
• Implémentabilité des automates temporisés

  2005cites this paper
• Lecture Notes in Computer Science: Preface

  2005cites this paper
• TWO PHASE TECHNIQUE FOR ASSEMBLY LINE BALANCING

  2005cites this paper
• Multi-clock timed networks

  2004cites this paper
• Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems

  2003cites this paper
• Hierarchical modeling and analysis of timed systems

  2003cites this paper
• Modeling and analysis of hybrid systems

  2003cites this paper
• Counterexample-guided predicate abstraction of hybrid systems

  2003cites this paper
• Model checking of systems with many identical timed processes

  2003cites this paper
• Linear parametric model checking of timed automata

  2001cites this paper
• Analyzing Real-Time Systems: Theory and Tools

  2001cites this paper
• Formal modelling and analysis of broadcasting embedded control systems

  2001cites this paper
• On Memory-Block Traversal Problems in Model-Checking Timed-Systems

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

  2000cites this paper
• Distributing Timed Model Checking - How the Search Order Matters

  2000cites this paper
• Efficient implementation of model-checkers for networks of timed automata

  2000cites this paper
• Predicate Diagrams for the Verification of Reactive Systems

  2000cites this paper
• Predicate Diagrams for the Verification of Real-Time Systems

  2000cites this paper
• Modelling and Veri cation of Real-Time Systems Using Timed Automata: Theory and Practice

  1999cites this paper
• Partial model checking of modal equations: A survey

  1999cites this paper
• A Tool Environment for The Development of Embedded Systems

  1999cites this paper
• Verifying Distributed LEGO RCX Programs Using UPPAAL

  1999cites this paper
• Splitting reachability analysis in hybrid automata

  1999cites this paper
• On the Existence of Network Invariants for Verifying Parameterized Systems

  1999cites this paper
• L'analyse formelle des systèmes temporisés en pratique. (The Formal Analysis of Timed Systems in Practice)

  1998cites this paper
• Modelling and analysis of broadcasting embedded control systems

  1998cites this paper
• Verifying Networks of Timed ProcessesParosh

  1998cites this paper
• of the Workshop on Applicability of Formal Methods AFM ’ 98 ( Aarhus , Denmark , June 2 , 1998 )

  1998cites this paper
• Clock Difference Diagrams

  1998cites this paper
• CMC: A Tool for Compositional Model-Checking of Real-Time Systems

  1998cites this paper
• Verifying Networks of Timed Processes (Extended Abstract)

  1998cites this paper
• Model Checking of Real-Time Reachability Properties Using Abstractions

  1998cites this paper
• Clock Di erence Diagrams

  1998cites this paper
• XTG-an engineering approach to modelling and analysis of real-time systems

  1998cites this paper
• Partition Refinement in Real-Time Model Checking

  1998cites this paper
• On Checking Parallel Real-time Systems for Linear Duration Properties on Checking Parallel Real-time Systems for Linear Duration Properties

  1998cites this paper
• Verification of Large State/Event Systems Using Compositionality and Dependency Analysis

  1998cites this paper
• On Checking Parallel Real-Time Systems for Linear Duration Properties

  1998cites this paper
• E cient Veri cation of Real-Time Systems: Compact Data Structure and State{Space Reduction

  1997cites this paper
• Paper D Eriication of Real-time Systems: Compact Data Structures and State-space Reduction. in Eecient Veriication of Real-time Systems: Com- Pact Data Structures and State-space Reduction

  1997cites this paper
• Continuous modeling of real-time and hybrid systems: from concepts to tools

  1997cites this paper
• Efficient verification of real-time systems: compact data structure and state-space reduction

  1997cites this paper
• Eecient Veriication of Real-time Systems: Compact Data Structures and State-space Reduction

  1997cites this paper
• UPPAAL: Status & Developments

  1997cites this paper
• Uppaal in a nutshell

  1997cites this paper
• Compositional Safety Logics

  1997cites this paper
• E cient Veri cation of Real-Time Systems : Compact Data Structure and State {

  1997cites this paper
• Modeling Sharing and Recursion for Weak Reduction Strategies Using Explicit Substitution

  1996cites this paper
• UPPAAL in 1995

  1996cites this paper
• UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

  1996cites this paper
• Diagnostic Model-Checking for Real-Time Systems

  1995cites this paper
• Compositional and symbolic model-checking of real-time systems

  1995cites this paper
• Forward and Time-Jumping Symbolic Model Checking for Real Time Systems

  year unknowncites this paper
• E(cid:14)cient Veri(cid:12)cation of Real-Time Systems: Compact Data Structure and State{Space Reduction

  year unknowncites this paper
• Clock Di(cid:11)erence Diagrams

  year unknowncites this paper