Paper Info
Title
Existential abstractions for distributed reactive systems via syntactic transformations
Abstract
Synchronous languages are well suited to implementation and verification of reactive systems. Large reactive systems tend to be distributed to cope with scalability and application specific demands. We propose abstractions for distributed reactive systems modelled as a set of synchronous nodes with asynchronous communication between them. The special features of synchronous programs allow us to obtain abstractions that are also valid synchronous programs only by syntactic transformations. For a given program, the set of all such abstractions forms a semi-lattice with the original program as the bottom and the most abstract program as the top element. The transformation we define is a natural basis for constructing an abstraction-refinement framework for verification. Given a program and a safety property, the abstraction-refinement process is a search in a lattice of programs obtained via syntactic transformations. We have implemented this abstraction refinement framework in a prototype tool and report our case studies.
Year
DOI
Venue
2007
10.1145/1289927.1289965
EMSOFT
Keywords
Field
DocType
valid synchronous program,synchronous node,abstract program,original program,reactive system,abstractions form,large reactive system,synchronous program,syntactic transformation,synchronous language,existential abstraction,distributed systems,real time systems,asynchronous communication
Asynchronous communication,Application specific,Abstraction,Programming language,Lattice (order),Computer science,Real-time computing,Reactive system,Syntax,Scalability,Safety property,Distributed computing
Conference
Citations 
PageRank 
References 
0
0.34
12
Authors
3
Name
Order
Citations
PageRank
Vijay D'Silva123914.07
Sampada Sonalkar2171.33
S. Ramesh3756.59