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 条

[31] Model-checking distributed real-time systems with states, events, and multiple fairness assumptions [J].

Wang, F .

ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 :553-567

[32] ASADAL/PROVER: A toolset for verifying temporal properties of real-time system specifications in statechart [J].

Ko, KI ;

Kang, KC .

IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1999, E82D (02) :398-411

[33] Efficient verification of parallel real-time systems [J].

Yoneda, T ;

Schlingloff, BH .

FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (02) :187-215

[34] Formal analysis of real-time systems with SAM [J].

Yu, HQ ;

He, XD ;

Deng, Y ;

Mo, LA .

FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2495 :275-286

[35] Compositional verification of embedded real-time systems [J].

Foughali, Mohammed ;

Hladik, Pierre-Emmanuel ;

Zuepke, Alexander .

JOURNAL OF SYSTEMS ARCHITECTURE, 2023, 142

[36] On Improved Verification of Reconfigurable Real-Time Systems [J].

Hafidi, Yousra ;

Kahloul, Laid ;

Khalgui, Mohamed ;

Ramdani, Mohamed .

PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON EVALUATION OF NOVEL APPROACHES TO SOFTWARE ENGINEERING (ENASE), 2019, :394-401

[37] Predicate Diagrams for the Verification of Real-Time Systems [J].

Kang, Eun-Young ;

Merz, Stephan .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 145 :151-165

[38] Symbolic simulation of real-time concurrent systems [J].

Wang, F ;

Huang, GD ;

Yu, F .

REAL-TIME AND EMBEDDED COMPUTING SYSTEMS AND APPLICATIONS, 2003, 2968 :595-617

[39] An incremental verification algorithm for real-time systems [J].

Sahay, A ;

Tsai, JJP ;

Sistla, AP .

INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 1999, 9 (02) :203-216

[40] Computing Accumulated Delays in Real-time Systems [J].

Rajeev Alur ;

Costas Courcoubetis ;

Thomas A. Henzinger .

Formal Methods in System Design, 1997, 11 :137-155

← 1 2 3 4 5 →