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 条

[21] Formalization and correctness of the PALS architectural pattern for distributed real-time systems
Meseguer, Jose
Olveczky, Peter Csaba
THEORETICAL COMPUTER SCIENCE, 2012, 451 : 1 - 37
[22] Specifying real-time properties in autonomic systems
Zhang, Ji
Zhou, Zhinan
Cheng, Betty H. C.
McKinley, Philip K.
INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2007, 3 (01) : 3 - 16
[23] Composition and refinement of discrete real-time systems
Ostroff, JS
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 1999, 8 (01) : 1 - 48
[24] TEMPORAL VERIFICATION OF REAL-TIME SYSTEMS
CAMPOS, SV
CLARKE, EM
MARRERO, W
MINEA, M
HIRAISHI, H
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1995, E78D (07) : 796 - 801
[25] REASONING ABOUT REAL-TIME SYSTEMS
PETERS, JF
AUSTRALIAN COMPUTER JOURNAL, 1993, 25 (04): : 135 - 147
[26] Verification of real-time systems design
Emilia Cambronero, M.
Valero, Valentin
Diaz, Gregorio
SOFTWARE TESTING VERIFICATION & RELIABILITY, 2010, 20 (01) : 3 - 37
[27] Observer Patterns for Real-Time Systems
Andre, Etienne
2013 18TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS), 2013, : 125 - 134
[28] Robust synthesis for real-time systems
Larsen, Kim G.
Legay, Axel
Traonouez, Louis-Marie
Wasowski, Andrzej
THEORETICAL COMPUTER SCIENCE, 2014, 515 : 96 - 122
[29] Verifying correctness of interfaces of design models of manufacturing systems using functional abstractions
Zurawski, R
IEEE TRANSACTIONS ON INDUSTRIAL ELECTRONICS, 1997, 44 (03) : 307 - 320
[30] Dense time-based model-checking of real-time systems
Zhang, GQ
Rong, M
PROCEEDINGS OF THE 11TH JOINT INTERNATIONAL COMPUTER CONFERENCE, 2005, : 785 - 788

← 1 2 3 4 5 →