Scenario-based verification of real-time systems using UPPAAL

DOI10.1007/s10703-010-0103-zzbMath1209.68323MaRDI QIDQ633291

Sandie Balaguer, Shuhao Li, Alexandre David, Brian Nielsen, Saulius Pusinskas, Kim Guldstrand 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

zbMATH Keywords

verification; modeling; timed automata; real-time system; scenario; live sequence chart

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Scenario-based verification of real-time systems using UPPAAL

Uses Software

• Kronos
• Uppaal

Cites Work

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