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 条

[41] Computing accumulated delays in real-time systems [J].

Alur, R ;

Courcoubetis, C ;

Henzinger, TA .

FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (02) :137-155

[42] Integer Parameter Synthesis for Real-Time Systems [J].

Jovanovic, Aleksandra ;

Lime, Didier ;

Roux, Olivier H. .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2015, 41 (05) :445-461

[43] Runtime verification of embedded real-time systems [J].

Reinbacher, Thomas ;

Fuegger, Matthias ;

Brauer, Joerg .

FORMAL METHODS IN SYSTEM DESIGN, 2014, 44 (03) :203-239

[44] An hybrid method for the validation of real-time systems [J].

Kaiser, L ;

Simonot-Lion, F .

FIELDBUS SYSTEMS AND THEIR APPLICATIONOS 2001 (FET'2001), 2002, :231-238

[45] An engineering process for the verification of real-time systems [J].

Burns, A. ;

Lin, T. -M. .

FORMAL ASPECTS OF COMPUTING, 2007, 19 (01) :111-136

[46] Error Finding in Real-Time Systems using Mutants of Temporal Properties [J].

Gonzalez, Ariel ;

Cristia, Maximiliano ;

Luna, Carlos .

2021 40TH INTERNATIONAL CONFERENCE OF THE CHILEAN COMPUTER SCIENCE SOCIETY (SCCC), 2021,

[47] Spatio-temporal model checking for mobile real-time systems [J].

Quesel, Jan-David ;

Schaefer, Andreas .

THEORETICAL ASPECTS OF COMPUTING - ICTAC 2006, 2006, 4281 :347-361

[48] Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions [J].

Lomuscio, Alessio ;

Michaliszyn, Jakub .

PROCEEDINGS OF THE 2015 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS (AAMAS'15), 2015, :189-198

[49] Towards a verifiable real-time, autonomic, fault mitigation framework for large scale real-time systems [J].

Dubey, Abhishek ;

Nordstrom, Steve ;

Keskinpala, Turker ;

Neema, Sandeep ;

Bapty, Ted ;

Karsai, Gabor .

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2007, 3 (01) :33-52

[50] Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude [J].

Bae, Kyungmin ;

Olveczky, Peter Csaba ;

Feng, Thomas Huining ;

Lee, Edward A. ;

Tripakis, Stavros .

SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (12) :1235-1271

← 1 2 3 4 5 →