Formal Methods for the Design of Real-Time Systems

DOI10.1007/B110123zbMath1105.68350OpenAlexW36240330MaRDI QIDQ5494310

Alexandre David, Gerd Behrmann, Kim Guldstrand Larsen

Publication date: 19 October 2006

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b110123

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (88)

Modelling and verification of weighted spiking neural systems ⋮ New Results on Timed Specifications ⋮ On Implementable Timed Automata ⋮ An integer static analysis for better extrapolation in Uppaal ⋮ Transformations for Compositional Verification of Assumption-Commitment Properties ⋮ Statistical Model Checking for Networks of Priced Timed Automata ⋮ An Abstract Model for Proving Safety of Autonomous Urban Traffic ⋮ Model Checking of Biological Systems ⋮ On the Modeling of Sequential Reactive Systems by Means of Real Time Automata ⋮ Automatic discovery of fair paths in infinite-state transition systems ⋮ Towards a formal semantics for UML/MARTE state machines based on hierarchical timed automata ⋮ Modular design of real-time systems using hierarchical communicating real-time state machines ⋮ Event algebra for transition systems composition application to timed automata ⋮ Specification and analysis of the AER/NCA active network protocol suite in real-time Maude ⋮ Distributed simulation of modular time Petri nets: An approach and a case study exploiting temporal uncertainty ⋮ Verifying autonomous systems ⋮ Axiomatisation and decidability of multi-dimensional Duration Calculus ⋮ Computational techniques for reachability analysis of Max-Plus-Linear systems ⋮ Semantics and pragmatics of real-time maude ⋮ A decidable timeout-based extension of linear temporal logic ⋮ Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems ⋮ Trace Analysis Using an Event-Driven Interval Temporal Logic ⋮ Bonding calculus ⋮ A model checking based approach to detect safety-critical adversarial examples on autonomous driving systems ⋮ Temporal Robustness of Stochastic Signals ⋮ Model-checking timed automata with deadlines with Uppaal ⋮ Timed Control with Observation Based and Stuttering Invariant Strategies ⋮ Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems ⋮ Analysing AWN-Specifications Using mCRL2 (Extended Abstract) ⋮ PuRSUE -- from specification of robotic environments to synthesis of controllers ⋮ Accelerating worst case execution time analysis of timed automata models with cyclic behaviour ⋮ Scenario-based verification of real-time systems using UPPAAL ⋮ Abstractions Refinement for Hybrid Systems Diagnosability Analysis ⋮ Superposition as a decision procedure for timed automata ⋮ Verification of graph grammars using a logical approach ⋮ Completeness for flat modal fixpoint logics ⋮ Distinguishing between communicating transactions ⋮ Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL} ⋮ Extended beam search for non-exhaustive state space analysis ⋮ Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets ⋮ Compositional Abstraction in Real-Time Model Checking ⋮ TCTL-preserving translations from timed-arc Petri nets to networks of timed automata ⋮ Improving active Mealy machine learning for protocol conformance testing ⋮ Employing Costs in Multiagent Systems with Timed Migration and Timed Communication ⋮ A formal approach to the WCRT analysis of multicore systems with memory contention under phase-structured task sets ⋮ Cost enforcement in the real-time specification for Java ⋮ Structural transformations for data-enriched real-time systems ⋮ Proving the existence of fair paths in infinite-state systems ⋮ Finding minimum and maximum termination time of timed automata models with cyclic behaviour ⋮ Models and formal verification of multiprocessor system-on-chips ⋮ A compositional modelling and analysis framework for stochastic hybrid systems ⋮ Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\) ⋮ Detecting synchronisation of biological oscillators by model checking ⋮ A menagerie of timed automata ⋮ Ensuring liveness properties of distributed systems: open problems ⋮ Formal Verification of Graph Grammars using Mathematical Induction ⋮ Reachability results for timed automata with unbounded data structures ⋮ Unnamed Item ⋮ A process calculus BigrTiMo of mobile systems and its formal semantics ⋮ An abstract model for proving safety of autonomous urban traffic ⋮ Remove irrelevant atomic formulas for timed automaton model checking ⋮ A modeling concept for formal verification of OS-based compositional software ⋮ Learning assumptions for compositional verification of timed automata ⋮ Max-entropy sampling for deterministic timed automata under linear duration constraints ⋮ Analysis of Linear Hybrid Systems in CLP ⋮ Optimal control strategies for stormwater detention ponds ⋮ Fast Directed Model Checking Via Russian Doll Abstraction ⋮ Analysing neurobiological models using communicating automata ⋮ Verification of Timed-Arc Petri Nets ⋮ Design and Verification of Fault-Tolerant Components ⋮ A situation-based multi-agent architecture for handling misunderstandings in interactions ⋮ Uppaal ⋮ An Introduction to Timed Automata ⋮ Dynamics of reputation in mobile agents systems and weighted timed automata ⋮ Analysis of a clock synchronization protocol for wireless sensor networks ⋮ A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata ⋮ Investigating the usability of real-time scheduling theory with the Cheddar project ⋮ Proving Safety of Traffic Manoeuvres on Country Roads ⋮ Towards an Efficient Tree Automata based technique for Timed Systems ⋮ Input urgent semantics for asynchronous timed session types ⋮ A flattening algorithm for hierarchical timed automata ⋮ Verification of Linear Duration Invariants by Model Checking CTL Properties ⋮ \textsc{LTL} falsification in infinite-state systems ⋮ Executable rewriting logic semantics of Orc and formal analysis of Orc programs ⋮ Unnamed Item ⋮ Automated formal analysis and verification: an overview ⋮ Abstraction and Completeness for Real-Time Maude ⋮ A lazy query scheme for reachability analysis in Petri nets

This page was built for publication: Formal Methods for the Design of Real-Time Systems