Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8 (1987)
Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering 23(5) (May 1997)
Harel, D., Naamad, A.: The STATEMATE semantics of Statecharts. ACM Trans. on Software Engineering and Methodology 5(4) (October 1996)
Berry, G., Gonthier, G.: The Esterel synchronous programming languages: Design, semantics, implementation. Science of Computer Programming 19(2), 87–152 (1992)
Ramesh, S.: Communicating Reactive State Machines: Design, Model & Implementation. In: IFAC Workshop on Distributed Computer Control Systems. Pergamon Press, Oxford (1998)
Berry, G., Ramesh, S., Shyamasundar, R.K.: Communicating Reactive Processes. In: 20th ACM Symposium on Principles of Programming Languages (1993)
Holzmann, G.J.: The Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Bhattacharjee, A.K., Dhodapkar, S.D., Seshia, S., Shyamasundar, R.K.: A graphical environment for the specification and verification of reactive systems. In: Felici, M., Kanoun, K., Pasquini, A. (eds.) SAFECOMP 1999. LNCS, vol. 1698, p. 431. Springer, Heidelberg (1999)
Bhattacharjee, A.K., Dhodapkar, S.D., Seshia, S., Shyamasundar, R.K.: PERTS: an environment for specification and verification of reactive systems. Reliability Engineering & Systems Safety Journal 71 (2001)
Seshia, S., Shyamasundar, R.K., Bhattacharjee, A.K., Dhodapkar, S.D.: SAFECOMP 1999. LNCS, vol. 1698. Springer, Heidelberg (1999)
Mikk, E., Lakhnech, S.M.: Hierarchical Automata as a model for Statecharts. In: Shyamasundar, R.K. (ed.) ASIAN 1997. LNCS, vol. 1345. Springer, Heidelberg (1997)
Mikk, E., Lakhnech, S.M., Holzmann, G.J.: Implementing Statecharts in Promela/SPIN. In: Proc. of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques. IEEE Computer Society, Los Alamitos, Technical Report (1999)
Bhattacharjee, A.K., Dhodapkar, S.D., Seshia, S., Shyamasundar, R.K.: STATEST: A Tool to Translate Statecharts to Esterel. BARC Technical Report. BARC/1998/E/014 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Iqbal, A., Bhattacharjee, A.K., Dhodapkar, S.D., Ramesh, S. (2003). Visual Modeling and Verification of Distributed Reactive Systems. In: Anderson, S., Felici, M., Littlewood, B. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2003. Lecture Notes in Computer Science, vol 2788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39878-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-39878-3_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20126-7
Online ISBN: 978-3-540-39878-3
eBook Packages: Springer Book Archive