Symbolic model checking for real-time systems

Finite-state programs over real-numbered time in a guarded-command language with real-valued clocks are described. Model checking answers the question of which states of a real-time program satisfy a branching-time specification. An algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space, is given.<<ETX>>

• Publication year

  1992

• Venue

  [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science

• Publication date

  1992-06-22

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1109/LICS.1992.185551
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• An algorithm computes the satisfying-state set symbolically as a fixpoint of a functional on state predicates without constructing the state space.

  Confidence 0.98

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• Symbolic model checking determines which states of a real-time program satisfy a branching-time specification.

  Confidence 0.95

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• Finite-state programs over real-numbered time are described in a guarded-command language with real-valued clocks.

  Confidence 0.97

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review

• algorithm

  method

  A procedure for computing the state set that satisfies the specification.

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• branching-time specification

  specification

  A specification formalism that can quantify over different execution branches from a state.

  Aliases: branching time specification

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• finite-state programs

  program model

  Programs described here as having finitely many states in a real-time setting.

  Aliases: finite-state program

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• fixpoint computation

  algorithm

  An iterative computation that finds a stable point of a functional over state predicates.

  Aliases: fixpoint of a functional

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• guarded-command language

  language

  A programming language organized around commands that execute when guards are satisfied.

  Aliases: guarded command language

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• real-numbered time

  time domain

  A time domain in which time values are real numbers.

  Aliases: real time

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• real-time program

  system model

  A program model that includes timing behavior and clock-based constraints.

  Aliases: real-time systems

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• real-valued clocks

  clock

  Clock variables whose values range over the real numbers.

  Aliases: real-valued clock

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• state predicates

  predicate

  Logical predicates used to denote sets of program states.

  Aliases: state predicate

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• state space

  state space

  The collection of all possible states of the program model.

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review
• symbolic model checking

  verification method

  Model checking performed by manipulating symbolic state sets rather than enumerating individual states.

  Aliases: symbolic verification

  박진우 (dztg5apj7m) extractionB (s683577b42) reviewjihoonc (k5vuy3tzcm) review

• Symbolic model checking

  1992cited by this paper
• Automatic verification of sequential circuit designs

  1992cited by this paper
• Minimization of Timed Transition Systems

  1992cited by this paper
• Compiling Real-Time Specifications into Extended Automata

  1992cited by this paper
• Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems

  1992cited by this paper
• Sooner is Safer Than Later

  1992cited by this paper
• An Approach to the Description and Analysis of Hybrid Systems

  1992cited by this paper
• Logics and Models of Real Time: A Survey

  1991cited by this paper
• Temporal proof methodologies for real-time systems

  1991cited by this paper
• Temporal and Modal Logic

  1991cited by this paper
• An Overview and Synthesis on Timed Process Algebras

  1991cited by this paper
• An old-fashioned recipe for real time

  1991cited by this paper
• Deciding Properties of Regular Real Time Processes

  1991cited by this paper
• The temporal specification and verification of real-time systems

  1991cited by this paper
• Techniques for automatic verification of real-time systems

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

  1990cited by this paper
• A logic of concrete time intervals

  1990cited by this paper
• Automata For Modeling Real-Time Systems

  1990cited by this paper
• A really temporal logic

  1989cited by this paper
• Verification of Synchronous Sequential Machines Based on Symbolic Execution

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

  1989cited by this paper
• Timing Assumptions and Verification of Finite-State Concurrent Systems

  1989cited by this paper
• Research on Automatic Verification of Finite-State Concurrent Systems

  1987cited by this paper
• Automatic verification of finite-state concurrent systems using temporal logic specifications

  1986cited by this paper
• “Sometimes” and “not never” revisited: on branching versus linear time temporal logic

  1986cited by this paper
• Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract)

  1986cited by this paper
• Graph-Based Algorithms for Boolean Function Manipulation

  1986cited by this paper
• Safety Without Stuttering

  1986cited by this paper
• A Unified Approach for Studying the Properties of Transition Systems

  1982cited by this paper
• Specification and verification of concurrent systems in CESAR

  1982cited by this paper
• Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons

  1982cited by this paper
• Results on the Propositional µ-Calculus

  1982cited by this paper
• Alternative Semantics for Temporal Logics

  1981cited by this paper
• Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic

  1981cited by this paper
• A Decision Procedure for the First Order Theory of Real Addition with Order

  1975cited by this paper

• Parametric Timed Bisimulation

  2020cites this paper
• Process mining approach to formal business process modelling and verification: a case study

  2020cites this paper
• Decidable ∃ *∀ * First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates

  2020cites this paper
• Pragmatic reuse for DSML development

  2020cites this paper
• Checking Timed Bisimulation with Bounded Zone-History Graphs - Technical Report

  2019cites this paper
• Sampling strategies for product lines with unbounded parametric real-time constraints

  2019cites this paper
• A framework for FMI-based co-simulation of human–machine interfaces

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

  2019cites this paper
• On Reconciling Schedulability Analysis and Model Checking in Robotics

  2019cites this paper
• MLν: A Distributed Real-Time Modal Logic

  2019cites this paper
• Connection models for the Internet-of-Things

  2019cites this paper
• Computing Bisimilarity Metrics for Probabilistic Timed Automata

  2019cites this paper
• Model Checking Longitudinal Control in Vehicle Platoon Systems

  2019cites this paper
• Computing Branching Distances Using Quantitative Games

  2019cites this paper
• Where are we now, and where do we go from here?

  2019cites this paper
• Statistical Model Checking of Complex Robotic Systems

  2019cites this paper
• Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata - Technical Report

  2019cites this paper
• Clock Bound Repair for Timed Systems

  2019cites this paper
• Applying Formal Methods to Verify Web Services Orchestration and Choreography

  2018cites this paper
• Time in SCCharts

  2018cites this paper
• Model Checking for Turn-Based Probability Epistemic Game Structure

  2018cites this paper
• Extended Automata for Temporal Planning of Interacting Agents

  2017cites this paper
• An Automatic Functional Coverage for Digital Systems Through a Binary Particle Swarm Optimization Algorithm with a Reinitialization Mechanism

  2017cites this paper
• Nested Timed Automata with Diagonal Constraints

  2017cites this paper
• Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

  2017cites this paper
• Using timed automata and fuzzy logic for diagnosis of multiple faults in DES

  2017cites this paper
• Anti-chain based algorithms for timed/probabilistic refinement checking

  2017cites this paper
• Chapter Three - Testing the Control-Flow, Data-Flow, and Time Aspects of Communication Systems: A Survey

  2017cites this paper
• Authoring and Automatic Verification of Interactive Multimedia Scores

  2017cites this paper
• Symbolic simulation of dataflow synchronous programs with timers

  2017cites this paper
• Nested Timed Automata with Invariants

  2017cites this paper
• Platform-Based Automotive Safety Features

  2016cites this paper
• Designing Schedulers for Hard Real-Time Tasks

  2016cites this paper
• Schedulability Analysis of Timed Regular Tasks by Under-Approximation on WCET

  2016cites this paper
• An efficient symbolic model checker

  2016cites this paper
• Formal Verification of the On-the-Fly Vehicle Platooning Protocol

  2016cites this paper
• Temporal Planning with Extended Timed Automata

  2016cites this paper
• Abstraction refinement and antichains for trace inclusion of infinite state systems

  2016cites this paper
• An Organizing System to Perform and Enable Verification and Diagnosis Activities

  2016cites this paper
• In the quantitative automata zoo

  2015cites this paper
• Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets

  2015cites this paper
• Timed Orchestration for Component-based Systems

  2015cites this paper
• Proper timed I/O: high-accuracy real-time control for conventional operating systems

  2015cites this paper
• Automated Verification of Stochastic Spiking Neural P Systems

  2015cites this paper
• Parametric multisingular hybrid Petri nets: Formal definitions and analysis techniques

  2015cites this paper
• Concluding remarks and future research directions

  2015cites this paper
• Correctness of Service Components and Service Component Ensembles

  2015cites this paper
• Modeling of Resilience Properties in Oscillatory Biological Systems Using Parametric Time Petri Nets

  2015cites this paper
• Formal Specification and Verification of Real-Time Multi-Agent Systems using Timed-Arc Petri Nets

  2015cites this paper
• leur gestion par utilisation d'outils de model-checking

  2015cites this paper
• Model Checking Web Services Choreography

  2015cites this paper
• Applying Rely/Guarantee in Compositional Ontology Alignment

  2014cites this paper
• Universit a degli Studi di Udine Dipartimento di Matematica e Informatica Dottorato di Ricerca in Informatica

  2014cites this paper
• A Graph-Based Transformation Reduction to Reach UPPAAL States Faster

  2014cites this paper
• On Compatibility Analysis of Inter Organizational Business Processes

  2014cites this paper
• Timed synchronizing sequences

  2014cites this paper
• Abstraction Refinement for Trace Inclusion of Infinite State Systems

  2014cites this paper
• Conceptual Modeling in Law: An Interdisciplinary Research Agenda

  2014cites this paper
• Runtime enforcement of regular timed properties

  2014cites this paper
• A SOC-Based Formal Specification and Verification of Hybrid Systems

  2014cites this paper
• Maximality-based Region Graph: A Novel Alternative

  2014cites this paper
• Modular safety veri cation and liveness testing of real-time industrial manufacturing systems using interval assumptions

  2014cites this paper
• True Concurrency Semantics: Towards a Verification of Timed Systems

  2014cites this paper
• Analyzing an embedded sensor with timed automata in uppaal

  2013cites this paper
• Models for Real-Time Embedded Systems

  2013cites this paper
• Formalization and Model Checking of SysML State Machine Diagrams by CSP#

  2013cites this paper
• A survey of timed automata for the development of real-time systems

  2013cites this paper
• A Timed Component Algebra for Services

  2013cites this paper
• Verification of Reachability Properties for Time Petri Nets

  2013cites this paper
• Model Checking Memory-Related Properties of Hardware/Software Co-designs

  2013cites this paper
• Timed Model-Checking

  2013cites this paper
• Artificial intelligence based cognitive routing for cognitive radio networks

  2013cites this paper
• Tools for Model-Checking Timed Systems

  2013cites this paper
• Real-Time Migration Properties of rTiMo Verified in Uppaal

  2013cites this paper
• Program Analysis as Model Checking

  2013cites this paper
• Trustworthy Software Development Based on Model Driven Architecture

  2013cites this paper
• An Introduction to Timed Automata

  2013cites this paper
• Modeling and verifying hierarchical real-time systems using stateful timed CSP

  2013influential citation
• Cancer Progression: Model, Therapy & Extraction

  2013cites this paper
• Employing Timed CTL assumptions in modular veri cation of invariant properties of real time component based systems

  2013cites this paper
• Improving Model Checking Stateful Timed CSP with non-Zenoness through Clock-Symmetry Reduction

  2013cites this paper
• Synchronous Abstract Machines

  2012cites this paper
• Integration of Safety Verification with Conformance Testing in Real-Time Reactive System

  2012cites this paper
• Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata

  2012cites this paper
• Verification and Analysis of Autonomic Systems for Networked Enterprises

  2012cites this paper
• REDUCING TIMED AUTOMATA : A NEW APPROACH

  2012cites this paper
• Parameter synthesis for hierarchical concurrent real-time systems

  2012cites this paper
• FIGI: floating interface for gesture-based interaction

  2012cites this paper
• A Parametric Counterexample Refinement Approach for Robust Timed Specifications

  2012cites this paper
• Dynamic Logics of Dynamical Systems

  2012cites this paper
• Process Calculus with Data Structure and its Model Checking Algorithm

  2012cites this paper
• Combining qualitative information and semi‐quantitative data for guaranteed invalidation of biochemical network models

  2012cites this paper
• Model checking of safety-critical software in the nuclear engineering domain

  2012cites this paper
• PR ESENT EE A

  2012cites this paper
• Principles of DEVS Model Verification for Real-Time Embedded Applications

  2012cites this paper
• Formal methods for practical reverse engineering and software verification

  2012cites this paper
• fonctions de support

  2012cites this paper
• A simple approach for reducing timed automata

  2012cites this paper
• Time Constraints with Temporal Logic Programming

  2012cites this paper
• An interactive virtual guide for the AR based visit of archaeological sites

  2011cites this paper