Scenario-based verification of real-time systems using UPPAAL

DOI10.1007/S10703-010-0103-ZzbMATH Open1209.68323OpenAlexW2146580567MaRDI QIDQ633291FDOQ633291

Authors: Shuhao Li, Sandie Balaguer, Alexandre David, Brian Nielsen, Saulius Pusinskas, Kim G. Larsen 

Publication date: 31 March 2011

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-010-0103-z

Recommendations

• scientific article; zbMATH DE number 1746447
• Formal Approaches to Software Testing
• scientific article; zbMATH DE number 1696448
• Uppaal in a nutshell
• Model-checking for real-time systems

zbMATH Keywords

verificationmodelingtimed automatareal-time systemscenariolive sequence chart

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Kronos: A verification tool for real-time systems
• Formal Methods for the Design of Real-Time Systems
• A theory of timed automata
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• LSCs: Breathing life into message sequence charts
• SYNTHESIZING STATE-BASED OBJECT SYSTEMS FROM LSC SPECIFICATIONS
• Title not available (Why is that?)
• Schedulability of asynchronous real-time concurrent objects
• Real-time system = discrete system + clock variables
• The computational complexity of scenario-based agent verification and design
• On the Expressive Power of Live Sequence Charts
• Title not available (Why is that?)
• Foundations of Software Science and Computation Structures
• Title not available (Why is that?)
• Check It Out: On the Efficient Formal Verification of Live Sequence Charts
• Verification of a radio-based signaling system using the STATEMATE verification environment
• Scenario-based verification of real-time systems using UPPAAL

Cited In (11)

• SMT-based scenario verification for hybrid systems
• Formal Approaches to Software Testing
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verification of the legOS scheduler using Uppaal
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Scenario-based verification of real-time systems using UPPAAL
• Scenario-based consistency verification of component-based real-time system designs
• Speeding up model checking of timed-models by combining scenario specialization and live component analysis

Uses Software

• Kronos
• Uppaal

This page was built for publication: Scenario-based verification of real-time systems using UPPAAL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q633291)