Scenario-based verification of real-time systems using Uppaal

被引：0
|
作者：
Shuhao Li
Sandie Balaguer
Alexandre David
Kim G. Larsen
Brian Nielsen
Saulius Pusinskas
机构：
[1] Aalborg University,CISS, Department of Computer Science
[2] ENS Cachan/INRIA,LSV
来源：
Formal Methods in System Design | 2010年 / 37卷
关键词：
Real-time system; Modeling; Timed automata; Scenario; Live sequence chart; Verification;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
This article proposes two approaches to tool-supported automatic verification of dense real-time systems against scenario-based requirements, where a system is modeled as a network of timed automata (TAs) or as a set of driving live sequence charts (LSCs), and a requirement is specified as a separate monitored LSC chart.
引用
收藏
页码：200 / 264
页数：64
相关论文
共 50 条
  • [1] Scenario-based verification of real-time systems using Uppaal
    Li, Shuhao
    Balaguer, Sandie
    David, Alexandre
    Larsen, Kim G.
    Nielsen, Brian
    Pusinskas, Saulius
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2010, 37 (2-3) : 200 - 264
  • [2] Scenario-Based Analysis and Synthesis of Real-Time Systems Using Uppaal
    Larsen, Kim G.
    Li, Shuhao
    Nielsen, Brian
    Pusinskas, Saulius
    [J]. 2010 DESIGN, AUTOMATION & TEST IN EUROPE (DATE 2010), 2010, : 447 - 452
  • [3] Verifying Real-Time Systems against Scenario-Based Requirements
    Larsen, Kim C.
    Li, Shuhao
    Nielsen, Brian
    Pusinskas, Saulius
    [J]. FM 2009: FORMAL METHODS, PROCEEDINGS, 2009, 5850 : 676 - 691
  • [4] Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems
    Boudjadar, Abdeldjalil
    Vaandrager, Frits
    Bodeveix, Jean-Paul
    Filali, Mamoun
    [J]. FUNDAMENTALS OF SOFTWARE ENGINEERING, FSEN 2013, 2013, 8161 : 111 - 132
  • [5] Using Uppaal for Verification of Priority Assignment in Real-Time Databases
    Kot, Martin
    [J]. DIGITAL INFORMATION PROCESSING AND COMMUNICATIONS, PT 2, 2011, 189 : 385 - 399
  • [6] Scaling up UPPAAL - Automatic verification of real-time systems using compositionality and abstraction
    Jensen, HE
    Larsen, KG
    Skou, A
    [J]. FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2000, 1926 : 19 - 30
  • [7] Modeling of Real-Time Embedded Systems using SysML and its Verification using UPPAAL and DiVinE
    Basit-Ur-Rahim, Muhammad Abdul
    Arif, Fahim
    Ahmad, Jamil
    [J]. 2014 5TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), 2014, : 132 - 136
  • [8] Online testing of real-time systems using UPPAAL
    Larsen, KG
    Mikucionis, M
    Nielsen, B
    [J]. FORMAL APPROACHES TO SOFTWARE TESTING, 2005, 3395 : 79 - 94
  • [9] Real-Time Simulation of Automotive Systems Based on UPPAAL
    Yan, Xuqin
    Li, Yanqiang
    Li, Xiaowei
    [J]. PROCEEDINGS OF 2017 8TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS 2017), 2017, : 173 - 176
  • [10] Temporal verification of Communicating Real-Time State Machines using Uppaal
    Furfaro, A
    Nigro, L
    [J]. 2003 IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL TECHNOLOGY, VOLS 1 AND 2, PROCEEDINGS, 2003, : 399 - 404
12345