Modular abstractions for verifying real-time distributed systems |
| |
Authors: | Hana De-Leon Orna Grumberg |
| |
Affiliation: | (1) Computer Science Department, The Technion, 32000 Haifa, Israel;(2) Present address: AT & T Bell Laboratories, 600 Mountain Avenue, Murray Hill, NJ, 07974 |
| |
Abstract: | 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 languageRTL is a branching-time version of the real-time temporal logicTPTL 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 ofRTL. |
| |
Keywords: | modular abstraction real-time distributed systems verification methodology model checking temporal logic |
本文献已被 SpringerLink 等数据库收录! |
|