Record Details

Visual modeling and verification of distributed reactive systems

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Visual modeling and verification of distributed reactive systems
 
Creator IQBAL, A
BHATTACHARJEE, AK
DHODAPKAR, SD
RAMESH, S
 
Description In this paper, we describe the design and implementation of a tool that has been developed for the specification and verification of distributed reactive systems. A distributed reactive system is composed of a collection of autonomous reactive nodes which communicate over buffered and/or unbuffered channels. Statecharts are industry accepted formal notation to model reactive systems but lack features to model communication. We have extended Statecharts [1], with primitives for handling communication through buffered and unbuffered channels. The extended notation is called Communicating Statecharts(CS). We have implemented a translator to translate CS into Promela, the input modeling language for the Spin model checker [2]. This allows us to verify temporal properties of the system using Spin model checker. As an illustrative example, we have modeled the well known Leader Election Protocol used in distributed systems using CS notation. The model was translated into Promela using the CSPROM tool and we have used the translated model in Promela to show the correctness of the algorithm by verifying its known properties. The verification was carried out using the Spin model checker. The contribution of the paper is in extending the powerful visual formalism of Statecharts with features required to model distributed systems and interfacing it with a well established model checking tool Spin for formal verification of the model.
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-23T15:16:04Z
2011-12-15T09:11:12Z
2011-10-23T15:16:04Z
2011-12-15T09:11:12Z
2003
 
Type Article; Proceedings Paper
 
Identifier COMPUTER SAFETY, RELIABILITY, AND SECURITY, PROCEEDINGS,2788,22-34
3-540-20126-2
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15160
http://hdl.handle.net/100/1922
 
Source 22nd International Conference on Computer Safety, Reliability and Security,EDINBURGH, SCOTLAND,SEP 23-26, 2003
 
Language English