Uppaal in a nutshell
From MaRDI portal
Publication:1856195
DOI10.1007/s100090050010zbMath1060.68577OpenAlexW2000947342MaRDI QIDQ1856195
Paul Pettersson, Wang Yi, Kim Guldstrand Larsen
Publication date: 1997
Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s100090050010
Related Items
Refinement of Timing Constraints for Concurrent Tasks with Scheduling, Quantitative Model Checking for a Controller Design, A case study on parametric verification of failure detectors, Revisiting Semantics of Interactions for Trace Validity Analysis, Verification of cooperating traffic agents, Safe and Optimal Adaptive Cruise Control, Performance Evaluation of Schedulers in a Probabilistic Setting, Performance Model Checking Scenario-Aware Dataflow, Robust Model-Checking of Timed Automata via Pumping in Channel Machines, Unnamed Item, Modeling for Verification, Model Checking Real-Time Systems, Symbolic Model Checking in Non-Boolean Domains, Parametric Deadlock-Freeness Checking Timed Automata, Formal Modeling and Analysis of Business Process Timed Constraints, Distributed parametric model checking timed automata under non-zenoness assumption, Simulation relations and applications in formal methods, Approximating Continuous Systems by Timed Automata, Optimal controller synthesis for timed systems, Unnamed Item, Energy Büchi problems, Wordgen : a Timed word Generation Tool, Parametric Verification of Weighted Systems, Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets, Timed Basic Parallel Processes, Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults, Progress-preserving Refinements of CTA, MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS, Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>, THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS, Testing timed automata, What’s Decidable About Parametric Timed Automata?, Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format, Scenario-Based Timing Consistency Checking for Time Petri Nets, Improvements for the Symbolic Verification of Timed Automata, Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking, One-Clock Deterministic Timed Automata Are Efficiently Identifiable in the Limit, A Kleene-Schützenberger Theorem for Weighted Timed Automata, Robust Analysis of Timed Automata Via Channel Machines, Modeling Routing Protocols in Adhoc Networks, Wireless ventilation control for large‐scale systems: The mining industrial case, An Inverse Method for Parametric Timed Automata, Model-checking Timed Temporal Logics, AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA, SAT-BASED MODEL CHECKING FOR REGION AUTOMATA, Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation, Stochastic Games for Verification of Probabilistic Timed Automata, Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker, Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints*, Discussion on: ``Formal specification method for systems automation, Timed recursive state machines: expressiveness and complexity, Presburger liveness verification of discrete timed automata., Timed hyperproperties, Explaining safety violations in real-time systems, \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability, Fast zone-based algorithms for reachability in pushdown timed automata, Scheduling with timed automata, Schedulability analysis of fixed-priority systems using timed automata, Updatable timed automata, Formalising concurrent UML state machines using coloured Petri nets, Parameter synthesis for probabilistic timed automata using stochastic game abstractions, On the optimal reachability problem of weighted timed automata, Verifying distributed real-time properties of embedded systems via graph transformations and model checking, On using priced timed automata to achieve optimal scheduling, Performance analysis of probabilistic timed automata using digital clocks, Analysis of a biphase mark protocol with Uppaal and PVS, Predictable real-time software synthesis, Schedulability of asynchronous real-time concurrent objects, Model checking of time Petri nets using the state class timed automaton, Rewriting modulo SMT and open system analysis, Distributed simulation of modular time Petri nets: An approach and a case study exploiting temporal uncertainty, Hybridization methods for the analysis of nonlinear systems, Modelling and analysis of normative documents, An engineering process for the verification of real-time systems, Semantics and pragmatics of real-time maude, Aspects of availability. Enforcing timed properties to prevent denial of service, Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata, Bounded Determinization of Timed Automata with Silent Transitions, Understand volatility of algorithmic stablecoin: modeling, verification and empirical analysis, Translating between models of concurrency, MR4UM: a framework for adding fault tolerance to UML state diagrams, Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems, Validation and verification of web services choreographies by using timed automata, Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving, The power of reachability testing for timed automata, Generalized discrete timed automata: Decidable approximations for safety verification., Pushdown timed automata: A binary reachability characterization and safety verification., Efficiently identifying deterministic real-time automata from labeled data, Collaborative models for autonomous systems controller synthesis, Bounded determinization of timed automata with silent transitions, A Kleene-Schützenberger theorem for weighted timed automata, Bisimulation conversion and verification procedure for goal-based control systems, Superposition as a decision procedure for timed automata, Computing branching distances with quantitative games, A concurrency-preserving translation from time Petri nets to networks of timed automata, Control: a perspective, Model-checking precision agriculture logistics: the case of the differential harvest, Integrating deployment architectures and resource consumption in timed object-oriented models, Robust reachability in timed automata and games: a game-based approach, Runtime enforcement of timed properties revisited, Parameter synthesis for hierarchical concurrent real-time systems, Cost enforcement in the real-time specification for Java, A design of GPU-based quantitative model checking, Models and formal verification of multiprocessor system-on-chips, Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata, Optimal reachability for multi-priced timed automata, An approximation algorithm for box abstraction of transition systems on real state spaces, Formal verification of multitasking applications based on timed automata model, Optimal infinite scheduling for multi-priced timed automata, Backward symbolic optimal reachability in weighted timed automata, Certifying emptiness of timed Büchi automata, Unnamed Item, Reconciling fault-tolerant distributed algorithms and real-time computing, Compositional schedulability analysis of real-time actor-based systems, A process algebraic framework for specification and validation of real-time systems, Optimal deployment of eventually-serializable data services, Timed modal logics for real-time systems. Specification, verification and control, The efficiency of identifying timed automata and the power of clocks, A brief history of process algebra, From LCF to Isabelle/HOL, Trading Plaintext-Awareness for Simulatability to Achieve Chosen Ciphertext Security, Identity-Based Hierarchical Key-Insulated Encryption Without Random Oracles, Design of a PLC control program for a batch plant VHS case study 1, Refinement and verification in component-based model-driven design, Towards verification of computation orchestration, M-nets: a survey, Formal verification of timed synchronous dataflow graphs using lustre, Uppaal, Formalized Timed Automata, Timed verification of the generic architecture of a memory circuit using parametric timed automata, Automatic symmetry detection for Promela, Verification of Asynchronous Circuits using Timed Automata, TPAP, Exact Acceleration of Real-Time Model Checking, Parking Can Get You There Faster, Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal, A theory of stochastic systems. I: Stochastic automata, A logical characterization of data languages., Translation Templates to Support Strategy Development in PVS, Relating Hybrid Chi to Other Formalisms, Recent Advances in Real-Time Maude, Is your model checker on time? On the complexity of model checking for timed modal logics, Automated verification of an audio-control protocol using UPPAAL, Linear parametric model checking of timed automata, Model-based Engineering of Embedded Systems Using the Hybrid Process Algebra Chi, Automatic verification of real-time systems with discrete probability distributions., Automatic Verification of Combined Specifications: An Overview, Abstraction and Completeness for Real-Time Maude, Specification of real-time and hybrid systems in rewriting logic, Checking timed Büchi automata emptiness efficiently
