Scenario-based verification of real-time systems using UPPAAL

DOI10.1007/S10703-010-0103-ZMaRDI QIDQ633291zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

live sequence chartmodelingreal-time systemscenariotimed automataverification

Mathematics Subject Classification ID

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

Recommendations

• UPPAAL -- now, next, and future
• Formal Approaches to Software Testing
• Verification of timed and hybrid systems
• Uppaal in a nutshell
• Model-checking for real-time systems

Cites work

• A theory of timed automata
• An automata based interpretation of live sequence charts
• Check It Out: On the Efficient Formal Verification of Live Sequence Charts
• Formal Methods for the Design of Real-Time Systems
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 5044575 (Why is no real title available?)
• Kronos: A verification tool for real-time systems
• LSCs: Breathing life into message sequence charts
• On the Expressive Power of Live Sequence Charts
• Real-time system = discrete system + clock variables
• Scenario-based monitoring and testing of real-time UML models
• Scenario-based verification of real-time systems using UPPAAL
• Schedulability of asynchronous real-time concurrent objects
• Smart play-out of behavioral requirements
• SYNTHESIZING STATE-BASED OBJECT SYSTEMS FROM LSC SPECIFICATIONS
• The computational complexity of scenario-based agent verification and design
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of a radio-based signaling system using the STATEMATE verification environment

Cited in

(11)

• SMT-based scenario verification for hybrid systems
• Verification of the legOS scheduler using Uppaal
• Verification of timed and hybrid systems
• Scaling up Uppaal. Automatic verification of real-time systems using compositionality and abstraction
• Speeding up model checking of timed-models by combining scenario specialization and live component analysis
• Scenario-based monitoring and testing of real-time UML models
• UPPAAL -- now, next, and future
• Verification of plan models using UPPAAL
• Scenario-based consistency verification of component-based real-time system designs
• Formal Approaches to Software Testing
• Scenario-based verification of real-time systems using UPPAAL

Describes a project that uses

Uses Software

• Uppaal
• Kronos

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)