MODULAR ABSTRACTIONS FOR VERIFYING REAL-TIME DISTRIBUTED SYSTEMS

被引：1
|
作者：
DELEON, H [1 ]
GRUMBERG, O [1 ]
机构：
[1] TECHNION ISRAEL INST TECHNOL,DEPT COMP SCI,IL-32000 HAIFA,ISRAEL
来源：
FORMAL METHODS IN SYSTEM DESIGN | 1993年 / 2卷 / 01期
关键词：
MODULAR ABSTRACTION; REAL-TIME DISTRIBUTED SYSTEMS; VERIFICATION METHODOLOGY; MODEL CHECKING; TEMPORAL LOGIC;
D O I：
10.1007/BF01383942
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this work we present a verification methodology for real-time distributed systems, based on their modular decomposition into processes. Given a distributed system, each of its components is reduced by abstracting away from details that are irrelevant for the required specification. The abstract components are then composed to form an abstract system to which a model checking procedure is applied. The abstraction relation and the specification language guarantee that if the abstract system satisfies a specification, then the original system satisfies it as well. The specification language RTL is a branching-time version of the real-time temporal logic TPTL presented in Alur and Henzinger [1]. Its model checking is linear in the size of the system and exponential in the size of the formula. Two notions of abstraction for real-time systems are introduced, each preserving a sublanguage of RTL.
引用
收藏
页码：7 / 43
页数：37
相关论文
共 50 条
  • [1] Modular abstractions for verifying real-time distributed systems
    [J]. De-Leon, Hana, 1600, (02):
  • [2] Verifying automata specification of distributed probabilistic real-time systems
    Luo Tiegeng
    Chen Huowang
    Wang Bingshan
    Wang Ji
    Gong Zhenghu
    Qi Zhichang
    [J]. Journal of Computer Science and Technology, 1998, 13 (6) : 588 - 596
  • [3] A modular approach to programming distributed real-time systems
    Ren, SP
    Agha, GA
    Saito, M
    [J]. JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 1996, 36 (01) : 4 - 12
  • [4] Influence of different abstractions on the performance analysis of distributed hard real-time systems
    Perathoner, Simon
    Wandeler, Ernesto
    Thiele, Lothar
    Hamann, Arne
    Schliecker, Simon
    Henia, Rafik
    Racu, Razvan
    Ernst, Rolf
    Gonzalez Harbour, Michael
    [J]. DESIGN AUTOMATION FOR EMBEDDED SYSTEMS, 2009, 13 (1-2) : 27 - 49
  • [5] Influence of different abstractions on the performance analysis of distributed hard real-time systems
    Simon Perathoner
    Ernesto Wandeler
    Lothar Thiele
    Arne Hamann
    Simon Schliecker
    Rafik Henia
    Razvan Racu
    Rolf Ernst
    Michael González Harbour
    [J]. Design Automation for Embedded Systems, 2009, 13 : 27 - 49
  • [6] Modular Design and Verification of Distributed Adaptive Real-Time Systems
    Goethel, Thomas
    Bartels, Bjoern
    [J]. NATURE OF COMPUTATION AND COMMUNICATION, 2015, 144 : 3 - 12
  • [7] Logic Based Abstractions of Real-Time Systems
    Roberto Barbuti
    Nicoletta De Francesco
    Antonella Santone
    Gigiola Vaglini
    [J]. Formal Methods in System Design, 2000, 17 : 201 - 220
  • [8] Logic based abstractions of real-time systems
    Barbuti, R
    De Francesco, N
    Santone, A
    Vaglini, G
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2000, 17 (03) : 201 - 220
  • [9] Formally specifying and verifying real-time systems
    Kemmerer, RA
    Kolano, PZ
    [J]. FIRST IEEE INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 1997, : 112 - 120
  • [10] Verifying timing constraints in real-time systems
    [J]. Bai, X. (baixy@tsinghua.edu.cn), 1600, Tsinghua University (52):
12345