Technical Report CS713
||MODULAR ABSTRACTIONS FOR VERIFYING REAL-TIME DISTRIBUTED SYSTEMS.
||H. De-Leon and O. Grumberg
|PDF - Revised||CS0713.revised.pdf|
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 [AH89]. 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.
|Copyright||The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information|
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/1992/CS/CS0713), rather than to the URL of the PDF or PS files directly. The latter URLs may change without notice.
To the list of the CS technical reports of 1992
To the main CS technical reports page
Computer science department, Technion