Checking Modal Contracts for Virtually Timed Ambients

  • Einar Broch Johnsen
  • Martin Steffen
  • Johanna Beate StumpfEmail author
  • Lars Tveito
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)


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.


  1. 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). Scholar
  2. 2.
    Akar, O.: Model checking of ambient calculus specifications against ambient logic formulas. Bachelor’s thesis, Istanbul Technical University (2009)Google Scholar
  3. 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). Scholar
  4. 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). Scholar
  5. 5.
    Baeten, J.C.M., Bergstra, J.A.: Real time process algebra. Form. Aspects Comput. 3(2), 142–188 (1991). Scholar
  6. 6.
    Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. Monographs in Theoretical Computer Science: An EATCS Series. Springer, Heidelberg (2002). Scholar
  7. 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).
  8. 8.
    Berger, M.: Towards abstractions for distributed systems. Ph.D. thesis, Imperial College, London (2004)Google Scholar
  9. 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).
  10. 10.
    Cardelli, L., Gordon, A.D.: Mobile ambients. Theor. Comput. Sci. 240(1), 177–213 (2000). Scholar
  11. 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). Scholar
  12. 12.
    Cardelli, L., Gordon, A.D.: Equational properties of mobile ambients. Math. Struct. Comput. Sci. 13(3), 371–408 (2003). Scholar
  13. 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). Scholar
  14. 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). Scholar
  15. 15.
    Ciobanu, G.: Interaction in time and space. Electron. Notes Theor. Comput. Sci. 203(3), 5–18 (2008). Scholar
  16. 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). Scholar
  17. 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).
  18. 18.
    Fibonacci. Greedy algorithm for Egyptian fractions.
  19. 19.
    Goldberg, R.P.: Survey of virtual machine research. IEEE Comput. 7(6), 34–45 (1974). Scholar
  20. 20.
    Gordon, A.D.: V for virtual. Electron. Notes Theor. Comput. Sci. 162, 177–181 (2006). Scholar
  21. 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). Scholar
  22. 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). Scholar
  23. 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). Scholar
  24. 24.
    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990). Scholar
  25. 25.
    Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. J. ACM 52(6), 961–1023 (2005). Scholar
  26. 26.
    Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebraic Program. 81(7–8), 721–781 (2012). Scholar
  27. 27.
    Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theor. Comput. Sci. 373(3), 213–237 (2007). Scholar
  28. 28.
    Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 685–695. Springer, Heidelberg (1992). Scholar
  29. 29.
    Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: theory and application. Inf. Comput. 114(1), 131–178 (1994). Scholar
  30. 30.
    Ölveczky, P.C.: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. UTCS. Springer, London (2017). Scholar
  31. 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).
  32. 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). Scholar
  33. 33.
    Prisacariu, C., Ciobanu, G.: Timed distributed \(\pi \)-calculus. Technical report, FML-05-01, Inst. of Computer Science Iasi (2005)
  34. 34.
    Rosa-Velardo, F., Segura, C., Verdejo, A.: Typed mobile ambients in maude. Electron. Notes Theor. Comput. Sci. 147(1), 135–161 (2006). Scholar
  35. 35.
    Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  36. 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). Scholar
  37. 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. 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).

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Einar Broch Johnsen
    • 1
  • Martin Steffen
    • 1
  • Johanna Beate Stumpf
    • 1
    Email author
  • Lars Tveito
    • 1
  1. 1.Inst. for informatikkUniversitetet i OsloOsloNorway

Personalised recommendations