Abstract
This paper presents a means to model and verify concurrent applications written in sC++. sC++ is an extension of C++ that adds concurrency to the language by unifying the object and task concepts into a single one, the active object. The management of active objects is the same as the management of usual C++ passive objects. The difference is that active objects have their own behaviour and that they may either accept method calls or call other objects 'methods. They are also capable to await simultaneously several non deterministic events including timers expiration. We show how to systematically model sC++ programs into Promela, a formal language supported by SPIN, a powerful and widely available model-checker. We present a classical example of a concurrent problem and give details about a tool that automatically produces the model from a program, verifies it and allows its debugging.
Chapter PDF
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
N. Begat, Réalisation d'un interface entre sC++ et SPIN, IIE, Evry, France, engineer report, in french, 1996.
G. Booch, J. Rumbaugh, I. Jacobson The UML User Guide, Add. Wesley, 1998.
T. Cartel, Modeling and Verification of a Multiprocessor Realtime OS Kernel, FORTE'94, Berne, 1994.
T. Cattel, Using Concurrency and Formal Methods for the Design of Safe Process Control. PDSE/ICSE-18 Workshop, Berlin, March 1996
J. Daems, Aide à l'engagement de centrales d'alarmes, EPFL engineer report, in french, 1995
G. Duval, Réalisation d'un debugger pour SPIN, report of MaÎtrise d'informatique, Université de BesanÇon, France, in french, 1994.
G. Duval, J. Julliand, Modeling and Verification of the RUBIS Micro-Kernel with SPIN, Proc. First SPIN Workshop, INRS Quebec, Canada, Oct. 1995.
G. Duval, T. Cattel, Specifying and Verifying the Steam Boiler Controler with SPIN. Springer-Verlag, LNCS vol. 1165, 1996.
G. Duval, T. Cattel, From Architecture down to Implementation of Safe Process Control Applications. HICSS-30 Wailea, Maui, Hawaii, U.S.A. 1997.
G. Duval, Specification and Verification of an Object Request Broker, submitted to ICSE, Kyoto, Japan, 1998.
C.A.R. Hoare, Monitors: An Operating System Structuring Concept, Communications of the ACM, 12(10), October 1974.
G.J. Holzmann, The Model Checker SPIN, IEEE Transactions on software engineering, vol. 23, no.5, May 1997.
J. Madsen, Validation and Testing of sC++ applications, IEEE conference Engineering of Computer Based Systems, Monterey, California, U.S.A. 1997.
C. Petitpierre, sC++, A Language Adapted to Interactive Applications, accepted for IEEE Computer Journal, March 1998. http://diwww.epfl.ch/w3lti/
K. Slonneger, B.L. Kurtz, Formal Syntax and Semantics of Programming Languages, Addison-Wesley, 1995.
C. West, Protocol validation by random state exploration. PSTV, VI, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cattel, T. (1998). Modeling and verification of sC++ applications. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054175
Download citation
DOI: https://doi.org/10.1007/BFb0054175
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive