Compositional and symbolic model-checking of real-time systems

Efficient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill (1990). However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables. In this paper we attack these explosion problems by developing and combining compositional and symbolic model-checking techniques. The presented techniques provide the foundation for a new automatic verification tool UPPAAL. Experimental results indicate that UPPAAL performs time- and space-wise favorably compared with other real-time verification tools.

• Publication year

  1995

• Venue

  Proceedings 16th IEEE Real-Time Systems Symposium

• Publication date

  1995-12-05

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1109/REAL.1995.495198
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

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

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

  1996cited by this paper
• A Compositional Proof of a Real-Time Mutual Exclusion Protocol

  1996cited by this paper
• Modeling Sharing and Recursion for Weak Reduction Strategies Using Explicit Substitution

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

  1995cited by this paper
• Compositional Model Checking of Real Time Systems

  1995cited by this paper
• Local Model Checking for Real-Time Systems (Extended Abstract)

  1995cited by this paper
• Partial model checking

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

  1995cited by this paper
• Verifying ET-LOTOS programmes with KRONOS

  1994influential reference
• A Theory of Timed Automata

  1994cited by this paper
• HYTECH: The Cornell HYbrid TECHnology Tool

  1994cited by this paper
• Delay Analysis in Synchronous Programs

  1993cited by this paper
• Timed Modal Specification - Theory and Tools

  1993cited by this paper
• Symmetry and model checking

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

  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
• An old-fashioned recipe for real time

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

  1990cited by this paper
• Model-checking for real-time systems

  1990influential reference
• A stubborn attack on state explosion

  1990cited by this paper
• Modelchecking for real-time systems

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

  1989influential reference
• The Use of Static Constructs in A Modal Process Logic

  1989cited by this paper
• A LATTICE-THEORETICAL FIXPOINT THEOREM AND ITS APPLICATIONS

  1955cited by this paper

• Research on Cache Coherence Protocol Verification Method Based on Model Checking

  2023influential citation
• Zone-based verification of timed automata: extrapolations, simulations and what next?

  2022cites this paper
• Formal analysis of timeliness in the RaSTA protocol

  2022cites this paper
• Activity report

  2019cites this paper
• In memory of Oded Maler: automatic reachability analysis of hybrid-state automata

  2019cites this paper
• A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems

  2019cites this paper
• Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle

  2019cites this paper
• Formal Verification of Protection Functions for Power Distribution Networks

  2018cites this paper
• Toward Implicit Learning for the Compositional Verification of Markov Decision Processes

  2018cites this paper
• Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process

  2018cites this paper
• A formal framework for the safe design of the Autonomous Driving supervision

  2018cites this paper
• Parameter Synthesis Problems for Parametric Timed Automata

  2018cites this paper
• Modelling of the real-time control system for a nuclear fusion experiment using Uppaal

  2017cites this paper
• A Comparative Assessment of Collaborative Business Process Verification Approaches

  2017cites this paper
• Relative time rates in dynamic timed automata

  2016cites this paper
• Verification column

  2016cites this paper
• Automatic compositional verification of probabilistic safety properties for inter-organisational workflow processes

  2016cites this paper
• Compositional verification of asynchronous concurrent systems using CADP

  2015cites this paper
• Automata and Logics for Concurrent Systems: Realizability and Verification

  2015cites this paper
• Multi-Hop Real-Time Communication over Switched Ethernet Technology

  2014cites this paper
• State Space Reconstruction in UPPAAL: An Algorithm and its Proof

  2014cites this paper
• Automata-theoretic modeling of fixed-priority non-preemptive scheduling for formal timing verification

  2014cites this paper
• Implementing a clock synchronization protocol on a multi-master Switched Ethernet network

  2013cites this paper
• State Space Reconstruction for On-Line Model Checking with UPPAAL

  2013cites this paper
• Timed Model-Checking

  2013cites this paper
• Scalable Compatibility for Embedded Real- Time components via Language Progressive Timed Automata

  2013cites this paper
• Modeling and Exploitation of Interaction and Concurrency

  2013cites this paper
• Algorithms and Data Structures for Efficient Timing Analysis of Asynchronous Real-time Systems

  2013cites this paper
• Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems

  2012cites this paper
• Formal verification of Intelligent Mechatronic Systems with decentralized control logic

  2012cites this paper
• Modeling and Exploitation of Interaction and Concurrency

  2012cites this paper
• Measuring Time Lag with Nested Preemptions and Resumptions

  2012cites this paper
• Emerald: An Automated Modeling and Verification Tool for Component-Based Real-Time Systems

  2012cites this paper
• Simulation framework for the verification of PLC programs in automobile industries

  2011cites this paper
• Flexible Plan Verification: Feasibility Results

  2011cites this paper
• Schedulability Analysis for Distributed Systems Using Network of Action Automata and Environment Automata

  2011cites this paper
• Closed-loop formal verification framework with non-determinism, configurable by meta-modelling

  2011cites this paper
• A new model for model checking: cycle-weighted Kripke structure

  2010influential citation
• Modeling and analysis of real -time systems with mutex components

  2010cites this paper
• Specification and Verification for Distributed and Timed Systems

  2010cites this paper
• Utilization of timed automata as a verification tool for real-time security protocols

  2010cites this paper
• Utilization of Timed Automata as a Verification Tool for Security Protocols

  2010cites this paper
• Transform Dual Transition Timed Petri Net into Timed Automaton for Model Checking with UPPAAL

  2010cites this paper
• Team MExICo Modelling and Exploitation of Interaction and Concurrency

  2010cites this paper
• Cybernetics in Software System Verification

  2009cites this paper
• From games to executables! Implementations of strategies generated from UPPAAL TIGA

  2009cites this paper
• Rigorous Development of Java Card Applications With the B Method

  2009cites this paper
• Environmental Simulation of Real-Time Systems with Nested Interrupts

  2009cites this paper
• Proceedings of Formal Methods 2009 Doctoral Symposium

  2009cites this paper
• Infinite Structures in Timed Systems

  2009cites this paper
• Verification Architectures for Real-time Systems ?

  2009cites this paper
• Modelling and Exploitation of Interaction and Concurrency

  2009cites this paper
• Control logic verification for an automotive body assembly line using simulation

  2009cites this paper
• Conditional models for compositional design of real-time embedded systems

  2008cites this paper
• Distributed Timed Automata with Independently Evolving Clocks

  2008cites this paper
• UCaS: A Schedulability Analysis Tool for AADL Models

  2008cites this paper
• Efficient Model-Checking of Dense-Time Systems with Time-Convexity Analysis

  2008cites this paper
• Simulation based control program verification in an automobile industry

  2008cites this paper
• Can Formal Methods Make Automotive Business Sense? A Classification of Formal Methods by Usefulness

  2008cites this paper
• The Verification of Real Time Systems Using the TINA Tool

  2008cites this paper
• Formal modeling and verification of shop floor controller logics

  2007cites this paper
• Åóð Òò × Óò×øöööòø Ëóðúúòò

  2007cites this paper
• Testing Time Goal-Driven Requirements with Model Checking Techniques

  2007cites this paper
• Validation and Veriication of Real Time Systems

  2007cites this paper
• Modeling, verification, and implementation of PLC program using timed-MPSG

  2007cites this paper
• An Abstraction Technique for Real-Time Verification

  2007cites this paper
• Model Checking: Software and Beyond

  2007cites this paper
• Task automata: Schedulability, decidability and undecidability

  2007cites this paper
• Sat-based Model Checking for Region Automata

  2006cites this paper
• Developing Reusable and Reconfigurable Real-Time Software using Aspects and Components

  2006cites this paper
• Modeling and Verification of a Time-triggered Networking Protocol

  2006cites this paper
• Analysis and Verification of Time Requirements Applied to the Web Services Composition

  2006cites this paper
• Integrating timed automata into tabu algorithm for HW-SW partitioning

  2006cites this paper
• A Mutation-based Framework for Automated Testing of Timeliness

  2006cites this paper
• Model based testing of real-time embedded components

  2006cites this paper
• A Supervisory Control Method for Ensuring the Conformance of Real-Time Discrete Event Systems

  2005cites this paper
• Tool Environment for Validation and Verification of Real-Time Systems

  2005cites this paper
• A Timing Analysis of AODV

  2005cites this paper
• Modular Verification of Reconfigurable Components

  2005cites this paper
• Over-approximate model of multitasking application based on timed automata using only one clock

  2005cites this paper
• Hybrid process algebra

  2005cites this paper
• Analysis of Real-Time Systems with CTL Model Checkers

  2005cites this paper
• A theory of stochastic systems part I: Stochastic automata

  2005cites this paper
• Verification of PLC Programs Given as Sequential Function Charts

  2004cites this paper
• Bounded Model Checking for Region Automata

  2004cites this paper
• Mutation-based testing criteria for timeliness

  2004cites this paper
• Supervisory control for the conformance of real-time discrete event systems 1 , 2

  2004cites this paper
• A Timed Extension for ALTARICA

  2004cites this paper
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems

  2004cites this paper
• Structural model checking

  2004cites this paper
• SUPERVISORY CONTROL FOR THE CONFORMANCE OF REAL-TIME DISCRETE EVENT SYSTEMS 1 , 2

  2004cites this paper
• Checking Temporal Business Rules

  2004influential citation
• Action and predicate safety of hybrid processes

  2004cites this paper
• A Generic Approach to Schedulability Analysis of Real-Time Tasks

  2004cites this paper
• Model Checking for Probabilistic Timed Systems

  2004cites this paper
• Validation of Stochastic Systems

  2004influential citation
• Toward Unbounded Model Checking for Region Automata

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

  2004cites this paper
• Models’ Validation for Complex Real-Time Systems

  2004cites this paper
• On the Urgency Expressiveness

  2004cites this paper