Abstract
We define a behavioural semantics for distributed Java applications and a procedure for building finite models of their behaviour. The models are synchronized networks of labelled transition systems, structured in a compositional way, and capturing the communication events between distributed objects. Our procedure is based on the analysis of the method call graph. If the set of observable events is made abstract enough to be finite, then our procedure is guaranteed to terminate and to compute a finite model.
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.
Similar content being viewed by others
References
Arnold, A.: Finite transition systems. Semantics of communicating sytems. Prentice-Hall, Englewood Cliffs (1994)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, p. 103. Springer, Heidelberg (2001)
Binkley, D., Gallagher, K.: Program slicing. Advances in Computers 43, 1–50 (1996)
Boulifa, R., Madelaine, E.: Finite model generation for distributed Java programs. In: Workshop on Model-Checking for Dependable Software-Intensive Systems, San-Francisco, June 2003, North-Holland, Amsterdam (2003)
Caromel, D., Klauser, W., Vayssi‘ere, J.: Towards seamless computing and metacomputing in Java. Concurrency Practice and Experience 10(11-13), 1043–1061 (1998)
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)
Cousot, P., Cousot, R.: Software analysis and model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 37–56. Springer, Heidelberg (2002)
Henrio, L., Caromel, D., Serpette, B.: Asynchronous and deterministic objects. In: Proceedings of the 31st ACM Symposium on Principles of Programming Languages, ACM Press, New York (2004) (to appear)
Dean, J., Grove, D., DeFouw, G., Chambers, C.: Call graph construction in objectoriented languages. In: Conference on Object-Oriented, pp. 108–124 (1997)
Hatcliff, J., Dwyer, M., Zheng, H.: Slicing software for model construction. Journal of High-order and Symbolic Computation (2000)
Roy, V., de Simone, R.: Auto and autograph. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 65–75. Springer, Heidelberg (1991); also available as RR-4460
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
Boulifa, R., Madelaine, E. (2004). Model Generation for Distributed Java Programs. In: Guelfi, N., Astesiano, E., Reggio, G. (eds) Scientific Engineering of Distributed Java Applications. FIDJI 2003. Lecture Notes in Computer Science, vol 2952. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24639-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-24639-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21091-7
Online ISBN: 978-3-540-24639-8
eBook Packages: Springer Book Archive