Abstract
Distributed Java applications use remote method invocation as a communication means between distributed objects. The ProActive library provides high level primitives and strong semantic guarantees for programming Java applications with distributed, mobile, secured components. We present a method for building finite, parameterized models capturing the behavioural semantics of ProActive objects. Our models are symbolic networks of labelled transition systems, whose labels represent (abstractions of) remote method calls. In contrast to the usual finite models, they encode naturally and finitely a large class of distributed object-oriented applications. Their finite instantiations can be used in classical model-checkers and equivalence-checkers for checking temporal logic properties in a compositional manner. We are building a software tool set for the analysis of ProActive applications using these methods.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-3-540-30232-2_24
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
Garavel, H., Lang, F.: NTIF: A general symbolic model for communicating sequential processes with data. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, Springer, Heidelberg (2002)
Arnold, A.: Finite transition systems. Semantics of communicating sytems. Prentice-Hall, Englewood Cliffs (1994)
Barros, T., Madelaine, E.: Formalisation and proofs of the chilean electronic invoices system. Technical Report RR-5217, INRIA (2004)
Boulifa, R., Madelaine, E.: Model generation for distributed Java programs. In: Guelfi, N., Astesiano, E., Reggio, G. (eds.) FIDJI 2003. LNCS, vol. 2952, pp. 139–152. Springer, Heidelberg (2004)
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Laubach, S., Zheng, H.: Bandera: Extracting finite-state models from java source code. In: Int. Conference on Software Engineering, ICSE (2000)
Cleaveland, R., Riely, J.: Testing-based abstractions for value-passing systems. In: International Conference on Concurrency Theory, pp. 417–432 (1994)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989) ISBN 0-13-114984-9.
Lakas, A.: Les Transformations Lotomaton: une contribution à la pré-implémentation des systémes Lotos. PhD thesis (1996)
Lin, H.: Symbolic transition graph with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, Springer, Heidelberg (1996)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Information and Computation 100 (1992)
Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The fc2tools set. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, Springer, Heidelberg (1994)
Caromel, D., Klauser, W., Vayssière, J.: Towards seamless computing and metacomputing in Java. Concurrency Practice and Experience 10, 1043–1061 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 IFIP International Federation for Information Processing
About this paper
Cite this paper
Barros, T., Boulifa, R., Madelaine, E. (2004). Parameterized Models for Distributed Java Objects. In: de Frutos-Escrig, D., Núñez, M. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2004. FORTE 2004. Lecture Notes in Computer Science, vol 3235. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30232-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-30232-2_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23252-0
Online ISBN: 978-3-540-30232-2
eBook Packages: Springer Book Archive