Scenario-based analysis and synthesis of real-time systems using uppaal

Abstract. We propose an approach to scenario-based analysis and synthesis of real-time embedded systems. The inter-process behaviors of a system are modeled as a set of driving universal Live Sequence Charts (LSCs), and the scenario-based user requirement is specified as a separate monitored universal or existential LSC. By translating the set of LSCs into a behavior-equivalent network of timed automata (TA), we reduce the problems of model consistency checking and property verification to CTL real-time model checking problems. Similarly, we reduce the problem of centralized synthesis for open systems to a timed game solving problem. We implement a prototype LSC-to-TA translator, which can be linked to our LSC editor and the existing real-time model checker Uppaal and timed game solver Uppaal-Tiga. Preliminary experiments on a number of examples and a case study show the applicability and effectiveness of this approach.

• Type: Conference
• Year: 2010
• Where: DATE
• Authors: Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas
• Keywords: DATE 2010, Hardware, Real-time Model, Real-time Model Checking, Timed Game