Skip to main content
SpringerLink
Log in
Book cover

Asian Symposium on Programming Languages and Systems

APLAS 2005: Programming Languages and Systems pp 401–417Cite as

A Parametric Model for the Analysis of Mobile Ambients

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3780))

Abstract

In this paper we propose a new parametric abstract finite model of Mobile Ambients able to express several properties on processes. The model can be used for the analysis of these properties by means of model checking techniques. The precision of the model can be increased by modifying certain numeric parameters increasingly avoiding thereby the occurrences of false counterexamples in the analysis.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Braghin, C., Cortesi, A., Focardi, R.: Control flow analysis of mobile ambients with security boundaries. In: Jacobs, B., Rensink, A. (eds.) FMOODS 2002, pp. 197–212. Kluwer, Dordrecht (2002)

    Google Scholar 

  2. Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  3. Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: POLP 2000, pp. 365–377. ACM Press, New York (2000)

    Google Scholar 

  4. Caires, L.: Behavioral and spatial observations in a logic for π-calculus. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 72–89. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. and Comp. 186(2), 194–235 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  6. Charatonik, W., Gordon, A.D., Talbot, J.-M.: Finite-control mobile ambients. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 295–313. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL 1977, pp. 238–252. ACM, New York (1977)

    Chapter  Google Scholar 

  8. Degano, P., Levi, F., Bodei, C.: Safe ambients: Control flow analysis and security. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 199–214. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. Distefano, D.: On model checking the dynamics of object-based software: a foundational approach. PhD thesis, University of Twente (November 2003)

    Google Scholar 

  10. Distefano, D.: A parametric model for the analysis of mobile ambients. Full version with proofs

    Google Scholar 

  11. Distefano, D., Katoen, J.-P., Rensink, A.: Who is pointing when to whom? on the automated verification of linked list structures. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 250–262. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Distefano, D., Rensink, A., Katoen, J.-P.: Who is pointing when to whom: on model-checking pointer structures. Tech. Report TR-CTIT-03-12, University of Twente (2003)

    Google Scholar 

  13. Hansen, R.R., Jensen, J.G., Nielson, F., Nielson, H.R.: Abstract interpretation of mobile ambients. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 134–148. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Levi, F., Maffeis, S.: An abstract interpretation framework for analysing mobile ambients. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 395–411. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  15. Levi, F., Sangiorgi, D.: Controlling interference in ambients. In: POPL 2000, pp. 352–364. ACM Press, New York (2000)

    Chapter  Google Scholar 

  16. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL 1985, pp. 97–107. ACM, New York (1985)

    Chapter  Google Scholar 

  17. Montanari, U., Pistore, M.: An introduction to history-dependent automata. In: Gordon, A., Pitts, A., Talcott, C. (eds.) HOOTS II. ENTCS, vol. 10. Elsevier Science Publishers, Amsterdam (1997)

    Google Scholar 

  18. Nielson, F., Nielson, H.R., Hansen, R.R., Jensen, J.G.: Validating farewalls in mobile ambients. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 463–477. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Pnueli, A.: The temporal logic of programs. In: Proceedings FOCS 1977, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)

    Google Scholar 

  20. Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. TOPLAS 20(1), 1–50 (1998)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Queen Mary, University of London,  

    Dino Distefano

Authors
  1. Dino Distefano
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Seoul National University, Korea

    Kwangkeun Yi

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Distefano, D. (2005). A Parametric Model for the Analysis of Mobile Ambients. In: Yi, K. (eds) Programming Languages and Systems. APLAS 2005. Lecture Notes in Computer Science, vol 3780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11575467_26

Download citation

  • DOI: https://doi.org/10.1007/11575467_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-29735-2

  • Online ISBN: 978-3-540-32247-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation