Abstract
Nowadays, many distributed applications take advantage of the transparent distributed object systems provided by CORBA middlewares. While greatly reduce the design and coding effort, the distributed object systems may also introduce subtle faults into the applications, which on the other hand, complicate the validation of the applications. In this paper, we present our work on applying SPIN to check the correctness of the designs of CORBA-based applications, taking into account those characteristics of CORBA that are essential to the correctness of the applications. In doing so, we provide adaptations to UML, so that the CORBA-based applications can be modeled with succinct yet sufficient details of the underlying middlewares. An automated translation tool is developed to generate Promela models from such UML design models. The translation tool embeds the behavioral details of the middleware automatically. In this way, the software developers can stay in their comfort zone while design faults, including those caused by the underlying distributed object systems can be pinpointed through the verification or the simulation with SPIN.
This is a preview of subscription content, log in via an institution to check access.
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
Cui, H.: Correctness of distributed systems with middleware. Master’s Thesis. School of Computer Science, University of Windsor (April 2003)
Duval, G.: Specification and verification of an object request broker. In: Proc. of the 20th International Conference on Software Engineering, pp. 43–52 (1998)
Garlan, D., Khersonsky, S., Kim, J.: Model checking publish-subscribe systems. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 166–180. Springer, Heidelberg (2003)
Hatcliff, J., Deng, X., Dwyer, M., Jung, G., Ranganath, V.P.: An integrated development, analysis, and verification environment for component-based systems. In: Proc. of the 25th International Conference on Software Engineering, pp. 160–173. IEEE, Los Alamitos (2003)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer 2(4), 366–381 (2000)
Holzmann, G.: The Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1991)
Holzmann, G.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5) (May 1997)
Kamel, M., Leue, S.: Formalization and validation of the general inter-ORB protocol (GIOP) using Promela and Spin. Software Tools for Technology Transfer 2(4), 394–409 (2000)
Kaveh, N., Emmerich, W.: Deadlock detection in distributed object systems. In: Proc. of the Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9), pp. 44–51. ACM Press, New York (2001)
Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computing 11, 637–664 (1999)
Lilius, J., Paltor, I.: Formalizing UML state machines for model checking. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 430–445. Springer, Heidelberg (1999)
Magee, J., Kramer, J.: Concurrency: Models and Programs – From Finite State Models to Java Programs. John Wiley, Chichester (1999)
Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.: Implementing statecharts in PROMELA/SPIN. In: Proc. of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, pp. 90–101 (1998)
Schafer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science 47, 1–13 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, J., Cui, H. (2004). Translation from Adapted UML to Promela for CORBA-Based Applications. In: Graf, S., Mounier, L. (eds) Model Checking Software. SPIN 2004. Lecture Notes in Computer Science, vol 2989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24732-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-24732-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21314-7
Online ISBN: 978-3-540-24732-6
eBook Packages: Springer Book Archive