Formal modeling and analysis of real-time resource-sharing protocols in Real-Time Maude

被引:0
|
作者
Olveczky, Peter Csaba [1 ]
Prabhakar, Pavithra [2 ]
Liu, Xue [3 ]
机构
[1] Univ Oslo, Dept Informat, N-0316 Oslo, Norway
[2] Univ Illinois, Dept Comp Sci, Urbana, IL USA
[3] McGill Univ, Sch Comp Sci, Montreal, PQ H3A 0G4, Canada
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
This paper presents general techniques for formally modeling, simulating, and model checking real-time resource-sharing protocols in Real-Time Maude. The "scheduling subset" of our techniques has been used to find a previously unknown subtle bug in a state-of-the-art scheduling algorithm. This paper also shows how our general techniques can be instantiated to model and analyze the well known priority inheritance protocol.
引用
收藏
页码:3774 / +
页数:2
相关论文
共 50 条
  • [1] Specification and analysis of real-time systems using Real-Time Maude
    Ölveczky, PC
    Meseguer, J
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2004, 2984 : 354 - 358
  • [2] Formal Analysis of Android Application Behavior with Real-Time Maude
    Nakajima, Shin
    [J]. 2015 IEEE 3RD INTERNATIONAL CONFERENCE ON CYBER-PHYSICAL SYSTEMS, NETWORKS, AND APPLICATIONS CPSNA 2015, 2015, : 7 - 12
  • [3] Synchronous AADL and Its Formal Analysis in Real-Time Maude
    Bae, Kyungmin
    Olveczky, Peter Csaba
    Al-Nayeem, Abdullah
    Meseguer, Jose
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, 2011, 6991 : 651 - +
  • [4] Resource Sharing Protocols for Real-Time Task Graph Systems
    Guan, Nan
    Ekberg, Pontus
    Stigge, Martin
    Yi, Wang
    [J]. PROCEEDINGS OF THE 23RD EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS (ECRTS 2011), 2011, : 272 - 281
  • [5] Formal Modeling and analysis of the OGDC wireless sensor network algorithm in real-time maude
    Oelveczky, Peter Csaba
    Thorvaldsen, Stian
    [J]. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, 2007, 4468 : 122 - +
  • [6] Semantics, Simulation, and Formal Analysis of Modeling Languages for Embedded Systems in Real-Time Maude
    Olveczky, Peter Csaba
    [J]. FORMAL MODELING: ACTORS, OPEN SYSTEMS, BIOLOGICAL SYSTEMS: ESSAYS DEDICATED TO CAROLYN TALCOTT ON THE OCCASION OF HER 70TH BIRTHDAY, 2011, 7000 : 368 - 402
  • [7] Towards formal modeling and analysis of networks of embedded medical devices in Real-Time Maude
    Olveczky, Peter Csaba
    [J]. PROCEEDINGS OF NINTH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, ARTIFICIAL INTELLIGENCE, NETWORKING AND PARALLEL/DISTRIBUTED COMPUTING, 2008, : 241 - 248
  • [8] Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude
    Olveczky, Peter Csaba
    Boronat, Artur
    Meseguer, Jose
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2010, 6117 : 47 - +
  • [9] Formal simulation and analysis of the CASH scheduling algorithm in real-time Maude
    Ölveczky, PC
    Caccamo, M
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 3922 : 357 - 372
  • [10] Formal semantics and efficient analysis of Timed Rebeca in Real-Time Maude
    Sabahi-Kaviani, Zeynab
    Khosravi, Ramtin
    Olveczky, Peter Csaba
    Khamespanah, Ehsan
    Sirjani, Marjan
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2015, 113 : 85 - 118