Advertisement

Checking Modal Contracts for Virtually Timed Ambients

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

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.

References

  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).  https://doi.org/10.1016/j.jss.2014.12.015CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-75292-9_4CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-74510-5_7CrossRefzbMATHGoogle Scholar
  5. 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/bf01898401CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-662-04995-2CrossRefzbMATHGoogle 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). http://www.usenix.org/events/osdi10/tech/full_papers/Ben-Yehuda.pdf
  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).  https://doi.org/10.1145/325694.325742
  10. 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-5MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/3-540-45413-6_8CrossRefGoogle Scholar
  12. 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/s0960129502003742MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/3-540-45315-6_10CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/3-540-44802-0_24CrossRefGoogle Scholar
  15. 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.083MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-540-71999-1CrossRefzbMATHGoogle 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).  https://doi.org/10.1109/cluster.2011.49
  18. 18.
    Fibonacci. Greedy algorithm for Egyptian fractions. https://en.wikipedia.org/wiki/Greedy_algorithm_for_Egyptian_fractions
  19. 19.
    Goldberg, R.P.: Survey of virtual machine research. IEEE Comput. 7(6), 34–45 (1974).  https://doi.org/10.1109/mc.1974.6323581CrossRefGoogle Scholar
  20. 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.030CrossRefGoogle 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).  https://doi.org/10.1016/j.jlamp.2014.07.001CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-319-72044-9_7CrossRefGoogle 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).  https://doi.org/10.1016/j.jlamp.2017.10.001MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990).  https://doi.org/10.1007/bf01995674CrossRefGoogle Scholar
  25. 25.
    Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. J. ACM 52(6), 961–1023 (2005).  https://doi.org/10.1145/1101821.1101825MathSciNetCrossRefzbMATHGoogle Scholar
  26. 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.003MathSciNetCrossRefzbMATHGoogle Scholar
  27. 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.018MathSciNetCrossRefzbMATHGoogle Scholar
  28. 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_114CrossRefGoogle Scholar
  29. 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.1083MathSciNetCrossRefzbMATHGoogle Scholar
  30. 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-0CrossRefzbMATHGoogle 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).  https://doi.org/10.2168/lmcs-3(1: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).  https://doi.org/10.1007/978-3-540-85778-5_1CrossRefGoogle Scholar
  33. 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. 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.041CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-02658-4_59CrossRefGoogle 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).  https://doi.org/10.1145/2168836.2168849

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

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

Personalised recommendations