Visual Modeling and Verification of Distributed Reactive Systems
| Autor: | S. Ramesh, S. D. Dhodapkar, A. K. Bhattacharjee, Asif Iqbal |
|---|---|
| Rok vydání: | 2003 |
| Předmět: |
Model checking
Correctness Programming language business.industry Computer science computer.software_genre UML state machine Promela Embedded system Formal specification SPIN model checker Visual modeling State diagram business computer Reactive system Formal verification computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783540201267 SAFECOMP |
| DOI: | 10.1007/978-3-540-39878-3_3 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|