Paper Info
Title
Verification of Distributed Object-Based Systems
Abstract
Distributed systems for open environments, like the Internet, are becoming more frequent and important. However, it is difficult to assure that such systems have the required functional properties. In this paper we use a visual formal specification language, called Object-Based Graph Grammars (OBGG), to specify asynchronous distributed systems. After discussing the main concepts of OBGG, we propose an approach for the verification of OBGG specifications using model checking. This approach consists on the translation of OBGG specifications into PROMELA (PROcess/PROtocol MEta LAnguage), which is the input language of the SPIN model checker. The approach we use for verification allows one to write properties based on the OBGG specification instead of on the generated PROMELA model.
Year
DOI
Venue
2003
10.1007/978-3-540-39958-2_18
Lecture Notes in Computer Science
Keywords
Field
DocType
model checking,distributed objects,distributed system
Rule-based machine translation,Distributed object,Programming language,Model checking,Computer science,Formal specification,Failure semantics,Theoretical computer science,Grammar systems theory,Promela,Distributed computing,SPIN model checker
Conference
Volume
ISSN
Citations 
2884
0302-9743
23
PageRank 
References 
Authors
1.26
9
4
Name
Order
Citations
PageRank
Fernando Luís Dotti110711.57
Luciana Foss29414.44
Leila Ribeiro329728.81
Osmar Marchi dos Santos41108.34