Parameterized Models for Distributed Java Objects

  • Tomás Barros
  • Rabéa Boulifa
  • Eric Madelaine
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3235)


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.


Active Object Label Transition System Abstract Domain Request Queue Future Object 
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.


  1. 1.
    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)Google Scholar
  2. 2.
    Arnold, A.: Finite transition systems. Semantics of communicating sytems. Prentice-Hall, Englewood Cliffs (1994)Google Scholar
  3. 3.
    Barros, T., Madelaine, E.: Formalisation and proofs of the chilean electronic invoices system. Technical Report RR-5217, INRIA (2004)Google Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    Cleaveland, R., Riely, J.: Testing-based abstractions for value-passing systems. In: International Conference on Concurrency Theory, pp. 417–432 (1994)Google Scholar
  7. 7.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989) ISBN 0-13-114984-9. zbMATHGoogle Scholar
  8. 8.
    Lakas, A.: Les Transformations Lotomaton: une contribution à la pré-implémentation des systémes Lotos. PhD thesis (1996)Google Scholar
  9. 9.
    Lin, H.: Symbolic transition graph with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, Springer, Heidelberg (1996)Google Scholar
  10. 10.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Information and Computation 100 (1992)Google Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Caromel, D., Klauser, W., Vayssière, J.: Towards seamless computing and metacomputing in Java. Concurrency Practice and Experience 10, 1043–1061 (1998)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2004

Authors and Affiliations

  • Tomás Barros
    • 1
  • Rabéa Boulifa
    • 1
  • Eric Madelaine
    • 1
  1. 1.INRIA Sophia-AntipolisFrance

Personalised recommendations