Abstract
Reactive Promela/RSPIN is an extension to the protocol validator Promela/SPIN. It enhances the simulation and verification capabilities of SPIN by allowing modular specifications to be analysed while alleviating the state-space explosion problem. Reactive Promela is a simple reactive language. The tool RSPIN is a preprocessor for SPIN which translates a Reactive Promela specification into a corresponding Promela specification. The main function performed by RSPIN is to combine configurations of Reactive Promela automata into Promela proctypes. The translated specification can then be simulated and verified using SPIN. We present our ideas first in a formal setting then we discuss their implementation in Reactive Promela and RSPIN concrete syntax and tool.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
C. André and L. Fancelli. A mixed (asynchronous / synchronous) implementation of a real-time system. In Euromicro 90, Amsterdam, 1990.
G. Berry and A. Benveniste. The synchronous approach to reactive and real-time systems. Another Look at Real Time Programming, Proceedings of the IEEE, 79:1270–1282, 1991.
Albert Benveniste, Paul Caspi, Paul Le Guernic, and Nicolas Halbwachs. Data-flow synchronous languages. Rapport de recherche 2089, INRIA, Unité de recherche INRIA Sophia-Antipolis, France, October 1993.
Frédéric Boussinot and Robert de Simone. The sl synchronous language. Rapport de recherche 2510, INRIA, Unité de recherche INRIA Sophia-Antipolis, France, Mars 1995.
G. Berry. Communicating reactive processes. In Proc. 20th ACM Conf. on Principles of Programming Languages, Charleston, Virginia, 1993.
G. Berry. The semantics of pure esterel. In Proc Marktoberdorf Intl. Summer School on Program Design Calculi, LNCS, to appear. Springer-Verlag, 1993.
G. Berry and G. Gonthier. Incremental development of an hdlc entity in Esterel. Comp. Networks and ISDN Systems, 22:35–49, 1991.
G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87–152, 1992.
S. Budkowski and E. Najm. Structured finite state automata, a new approach for modelling distributed communication systems. In H. Rudin and C. H. West, editors, Protocol Specification, Testing and Verification, III. Elsevier Science Publishers B.V (North-Holland), 1983.
F. Boussinot. Reactive c: An extension of c to program reactive systems. Software-Practice and Experience, 21(4):401–428, 1991.
P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. Lustre, a declarative language for programming synchronous systems. In Proceedings of ACM Conference on Principles of Programming Languages, ACM, 1985.
Monica Lara de Souza and Robert de Simone. Using po methods for verifying behavioural equivalences. In Proceedings of FORTE'95, pages 59–74, October 1995.
Jean-Claude Fernandez. Aldebaran: A tool for verification of communicating processes. Rapport SPECTRE C14, Laboratoire de Génie Informatique — Institut IMAG, Grenoble, September 1989.
R. Gerth, R. Kuiper, R. Peled, and W. Penczek. A partial order approach to branching time model checking. In Proceedings of ISTCS, pages 330–339, 1995.
Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. PhD thesis, UNIVERSITE DE LIEGE, Faculté des Sciences Appliquées, 1994.
P. Le Guernic. Signal, a data-flow oriented language for signal processing. IEEE Trans. ASSP, 34(2):362–374, 1986.
N. Halbswachs. Synchronous Programming of Reactive Systems. Kluwer Academic Press, Netherlands, 1993.
Gerhard Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, N.J., first edition, 1991.
M. Jourdan, F. Lagnier, P. Raymond, and F. Maraninchi. A multiparadigm language for reactive systems.
E. Madelaine. Verification tools from the Concur project. EATCS Bulletin, 47, 1992.
E. Madelaine and D. Vergamini. Auto: A verification tool for distributed systems using reduction of finite automata networks. In Proc. FORTE'89 Conference, Vancouver, 1989.
D. Peled. Combining partial order reductions with on-the-fly model-checking. In Proceedings of CAV'94, LNCS 818. Springer-Verlag, 1994.
G. Plotkin. A structural approach to operational semantics. Technical report, Comput. Sci. Dept., Aarhus Univ., 1981.
V. Roy and R. de Simone. Auto and autograph. In R. Kurshan, editor, proceedings of Workshop on Computer Aided Verification, New-Brunswick, June 1990. AMS-DIMACS.
A. Valmari. A stubborn attack on state explosion. LNCS 531. Springer-Verlag, 1990.
P. Wolper and P. Godefroid. Partial order methods for temporal verification. In Proceedings of Concur'93, LNCS 715. Springer-Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Najm, E., Olsen, F. (1996). Reactive EFSMs — Reactive Promela/RSPIN. In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_54
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_54
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61042-7
Online ISBN: 978-3-540-49874-2
eBook Packages: Springer Book Archive