Skip to main content
SpringerLink
Log in

Checking Modal Contracts for Virtually Timed Ambients

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2018 (ICTAC 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11187))

Included in the following conference series:

Abstract

The calculus of virtually timed ambients models timing aspects of resource management for virtual machines. With nested virtualization, virtual machines compete with other processes for the resources of their host environment. Resource provisioning in virtually timed ambients can be formalized by extending the capabilities of mobile ambients to model the dynamic creation, migration, and destruction of virtual machines. This paper introduces a logic to define modal contracts regarding resource management for virtually timed ambients. Service-level agreements are contracts between a service provider and a client, specifying properties that the service should fulfill with respect to quality of service (QoS). The proposed modal logic supports QoS statements about the resource consumption and nesting structure of a system during the timed reduction of its processes. Besides a formal definition of the logic, the paper provides a corresponding model checking algorithm and its prototype implementation in rewriting logic.

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

Access this chapter

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

Institutional subscriptions

Notes

  1. 1.

    The full source code is available at https://github.com/larstvei/Check-VTA/tree/modal-contracts.

References

  1. Abdelmaboud, A., Jawawi, D.N., Ghani, I., Elsafi, A., Kitchenham, B.: Quality of service approaches in cloud computing: a systematic mapping study. J. Syst. Softw. 101, 159–179 (2015). https://doi.org/10.1016/j.jss.2014.12.015

    Article  Google Scholar 

  2. Akar, O.: Model checking of ambient calculus specifications against ambient logic formulas. Bachelor’s thesis, Istanbul Technical University (2009)

    Google Scholar 

  3. Aman, B., Ciobanu, G.: Mobile ambients with timers and types. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 50–63. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75292-9_4

    Chapter  Google Scholar 

  4. Aman, B., Ciobanu, G.: Timers and proximities for mobile ambients. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol. 4649, pp. 33–43. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74510-5_7

    Chapter  MATH  Google Scholar 

  5. Baeten, J.C.M., Bergstra, J.A.: Real time process algebra. Form. Aspects Comput. 3(2), 142–188 (1991). https://doi.org/10.1007/bf01898401

    Article  MATH  Google Scholar 

  6. Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. Monographs in Theoretical Computer Science: An EATCS Series. Springer, Heidelberg (2002). https://doi.org/10.1007/978-3-662-04995-2

    Book  MATH  Google Scholar 

  7. Ben-Yehuda, M., et al.: The turtles project: design and implementation of nested virtualization. In: Proceedings of 9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, Vancouver, BC, October 2010, pp. 423–436. USENIX Association (2010). http://www.usenix.org/events/osdi10/tech/full_papers/Ben-Yehuda.pdf

  8. Berger, M.: Towards abstractions for distributed systems. Ph.D. thesis, Imperial College, London (2004)

    Google Scholar 

  9. Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: Proceedings of 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2000, Boston, MA, January 2000, pp. 365–377. ACM Press, New York (2000). https://doi.org/10.1145/325694.325742

  10. Cardelli, L., Gordon, A.D.: Mobile ambients. Theor. Comput. Sci. 240(1), 177–213 (2000). https://doi.org/10.1016/s0304-3975(99)00231-5

    Article  MathSciNet  MATH  Google Scholar 

  11. Cardelli, L., Gordon, A.D.: Logical properites of name restriction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 46–60. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45413-6_8

    Chapter  Google Scholar 

  12. Cardelli, L., Gordon, A.D.: Equational properties of mobile ambients. Math. Struct. Comput. Sci. 13(3), 371–408 (2003). https://doi.org/10.1017/s0960129502003742

    Article  MathSciNet  MATH  Google Scholar 

  13. Charatonik, W., Dal Zilio, S., Gordon, A.D., Mukhopadhyay, S., Talbot, J.-M.: The complexity of model checking mobile ambients. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 152–167. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45315-6_10

    Chapter  MATH  Google Scholar 

  14. Charatonik, W., Talbot, J.-M.: The decidability of model checking mobile ambients. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 339–354. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_24

    Chapter  Google Scholar 

  15. Ciobanu, G.: Interaction in time and space. Electron. Notes Theor. Comput. Sci. 203(3), 5–18 (2008). https://doi.org/10.1016/j.entcs.2008.04.083

    Article  MathSciNet  MATH  Google Scholar 

  16. Clavel, M.: All About Maude - A High-Performance Logical Framework, How to Specify, Program, and Verify Systems in Rewriting Logic. Programming and Software Engineering, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1

    Book  MATH  Google Scholar 

  17. Crago, S., et al.: Heterogeneous cloud computing. In: Proceedings of 2011 IEEE International Conference on Cluster Computing, Austin, TX, September 2011, pp. 378–385. IEEE CS Press, Washington, DC (2011). https://doi.org/10.1109/cluster.2011.49

  18. Fibonacci. Greedy algorithm for Egyptian fractions. https://en.wikipedia.org/wiki/Greedy_algorithm_for_Egyptian_fractions

  19. Goldberg, R.P.: Survey of virtual machine research. IEEE Comput. 7(6), 34–45 (1974). https://doi.org/10.1109/mc.1974.6323581

    Article  Google Scholar 

  20. Gordon, A.D.: V for virtual. Electron. Notes Theor. Comput. Sci. 162, 177–181 (2006). https://doi.org/10.1016/j.entcs.2006.01.030

    Article  Google Scholar 

  21. Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: Integrating deployment architectures and resource consumption in timed object-oriented models. J. Log. Algebraic Methods Program. 84(1), 67–91 (2015). https://doi.org/10.1016/j.jlamp.2014.07.001

    Article  MATH  Google Scholar 

  22. Johnsen, E.B., Steffen, M., Stumpf, J.B.: A calculus of virtually timed ambients. In: James, P., Roggenbach, M. (eds.) WADT 2016. LNCS, vol. 10644, pp. 88–103. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72044-9_7

    Chapter  Google Scholar 

  23. Johnsen, E.B., Steffen, M., Stumpf, J.B.: Virtually timed ambients: a calculus of nested virtualization. J. Log. Algebraic Methods Program. 94, 109–127 (2018). https://doi.org/10.1016/j.jlamp.2017.10.001

    Article  MathSciNet  MATH  Google Scholar 

  24. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990). https://doi.org/10.1007/bf01995674

    Article  Google Scholar 

  25. Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. J. ACM 52(6), 961–1023 (2005). https://doi.org/10.1145/1101821.1101825

    Article  MathSciNet  MATH  Google Scholar 

  26. Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebraic Program. 81(7–8), 721–781 (2012). https://doi.org/10.1016/j.jlap.2012.06.003

    Article  MathSciNet  MATH  Google Scholar 

  27. Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theor. Comput. Sci. 373(3), 213–237 (2007). https://doi.org/10.1016/j.tcs.2006.12.018

    Article  MathSciNet  MATH  Google Scholar 

  28. Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 685–695. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55719-9_114

    Chapter  Google Scholar 

  29. Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: theory and application. Inf. Comput. 114(1), 131–178 (1994). https://doi.org/10.1006/inco.1994.1083

    Article  MathSciNet  MATH  Google Scholar 

  30. Ölveczky, P.C.: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. UTCS. Springer, London (2017). https://doi.org/10.1007/978-1-4471-6687-0

    Book  MATH  Google Scholar 

  31. Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Log. Methods Comput. Sci. 3(1), Article 8 (2007). https://doi.org/10.2168/lmcs-3(1:8)2007

  32. Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85778-5_1

    Chapter  Google Scholar 

  33. Prisacariu, C., Ciobanu, G.: Timed distributed \(\pi \)-calculus. Technical report, FML-05-01, Inst. of Computer Science Iasi (2005) http://iit.iit.tuiasi.ro/TR/reports/fml1501.pdf

  34. Rosa-Velardo, F., Segura, C., Verdejo, A.: Typed mobile ambients in maude. Electron. Notes Theor. Comput. Sci. 147(1), 135–161 (2006). https://doi.org/10.1016/j.entcs.2005.06.041

    Article  MATH  Google Scholar 

  35. Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    MATH  Google Scholar 

  36. Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_59

    Chapter  Google Scholar 

  37. Sun, Y.: Toward a model checker for ambient logic using the process analysis toolkit. MSc thesis, Bishop’s University, Sherbrooke, Quebec (2015)

    Google Scholar 

  38. Williams, D., Jamjoom, H., Weatherspoon, H.: The Xen-Blanket: virtualize once, run everywhere. In: Proceedings of 7th European Conference on Computer Systems, EuroSys 2012, Bern, April 2012, pp. 113–126. ACM Press, New York (2012). https://doi.org/10.1145/2168836.2168849

Download references

Author information

Authors and Affiliations

  1. Inst. for informatikk, Universitetet i Oslo, Postboks 1080, Blindern, 0316, Oslo, Norway

    Einar Broch Johnsen, Martin Steffen, Johanna Beate Stumpf & Lars Tveito

Authors
  1. Einar Broch Johnsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Johanna Beate Stumpf
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lars Tveito
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Johanna Beate Stumpf .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  2. Reykjavík University, Reykjavik, Iceland

    Tarmo Uustalu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Johnsen, E.B., Steffen, M., Stumpf, J.B., Tveito, L. (2018). Checking Modal Contracts for Virtually Timed Ambients. In: Fischer, B., Uustalu, T. (eds) Theoretical Aspects of Computing – ICTAC 2018. ICTAC 2018. Lecture Notes in Computer Science(), vol 11187. Springer, Cham. https://doi.org/10.1007/978-3-030-02508-3_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02508-3_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02507-6

  • Online ISBN: 978-3-030-02508-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation