Skip to main content
SpringerLink
Log in

Using Coloured Petri Nets for Resource Analysis of Active Objects

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2018)

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

Included in the following conference series:

Abstract

Pay-on-demand resource provisioning is an important driver for cloud computing. Virtualized resources in cloud computing open for resource awareness, such that applications may contain resource management strategies to modify their deployment and reduce resource consumption. The ABS language supports the modelling of deployment decisions and resource management for active objects. In this paper, the semantics of ABS is captured directly as a Coloured Petri Net (CPN) model capable of representing any ABS program by an appropriate initial marking. We define an abstraction relation between the CPN model and the language semantics such that markings of the CPN model become abstract ABS configurations. We use a CPN model checker as an abstract interpreter to investigate resource distribution and starvation problems for deployed active objects in ABS.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and 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

Institutional subscriptions

References

  1. Agha, G., Hewitt, C.: Concurrent programming using actors. Object-Oriented Concurrent Programming, pp. 37–53. The MIT Press, Cambridge (1987)

    Google Scholar 

  2. Agha, G.: ACTORS: A Model of Concurrent Computations in Distributed Systems. The MIT Press, Cambridge (1986)

    Google Scholar 

  3. Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142–159 (2012)

    Article  MathSciNet  Google Scholar 

  4. Albert, E., et al.: Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS. J. Serv.-Oriented Comput. Appl. 8(4), 323–339 (2014)

    Article  Google Scholar 

  5. Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf, Dallas (2007)

    Google Scholar 

  6. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76–85 (2010)

    Article  Google Scholar 

  7. Barbanera, F., Bugliesi, M., Dezani-Ciancaglini, M., Sassone, V.: Space-aware ambients and processes. Theor. Comput. Sci. 373(1–2), 41–69 (2007)

    Article  MathSciNet  Google Scholar 

  8. Bjørk, J., de Boer, F.S., Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: User-defined schedulers for real-time concurrent objects. Innov. Syst. Softw. Eng. 9(1), 29–43 (2013)

    Article  Google Scholar 

  9. de Boer, F., et al.: A survey of active object languages. ACM Comput. Surv. 50(5), 76:1–76:39 (2017)

    Article  Google Scholar 

  10. de Boer, F.S., Bravetti, M., Grabe, I., Lee, M., Steffen, M., Zavattaro, G.: A petri net based analysis of deadlocks for active objects and futures. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 110–127. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35861-6_7

    Chapter  Google Scholar 

  11. de Boer, F.S., Bravetti, M., Lee, M.D., Zavattaro, G.: A petri net based modeling of active objects and futures. Fundam. Inform. 159(3), 197–256 (2018)

    Article  MathSciNet  Google Scholar 

  12. de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_22

    Chapter  Google Scholar 

  13. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Quantitative analysis of real-time systems using priced timed automata. Commun. ACM 54(9), 78–87 (2011)

    Article  Google Scholar 

  14. Brogi, A., Canciani, A., Soldani, J., Wang, P.: Petri net-based approach to model and analyze the management of cloud applications. ToPNoC XI, 28–48 (2016)

    MathSciNet  Google Scholar 

  15. Bruni, R., Melgratti, H., Tuosto, E.: Translating orc features into petri nets and the join calculus. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 123–137. Springer, Heidelberg (2006). https://doi.org/10.1007/11841197_8

    Chapter  Google Scholar 

  16. Caromel, D., Henrio, L.: A Theory of Distributed Objects. Springer, Berlin (2005). https://doi.org/10.1007/b138812

    Book  MATH  Google Scholar 

  17. Din, C.C., Bubel, R., Hähnle, R.: KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 517–526. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_35

    Chapter  Google Scholar 

  18. Din, C.C., Owe, O.: Compositional reasoning about active objects with shared futures. Formal Asp. Comput. 27(3), 551–572 (2015)

    Article  MathSciNet  Google Scholar 

  19. Gkolfi, A., Din, C.C., Johnsen, E.B., Steffen, M., Yu, I.C.: Translating active objects into colored petri nets for communication analysis. In: Dastani, M., Sirjani, M. (eds.) FSEN 2017. LNCS, vol. 10522, pp. 84–99. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68972-2_6

    Chapter  Google Scholar 

  20. Gkolfi, A., Johnsen, E.B., Kristensen, L.M., Yu, I.C.: Using coloured petri nets for resource analysis of active objects (full version). Technical report 484, Department of informatics, University of Oslo (2018)

    Google Scholar 

  21. Gordon, A.D. (ed.): ESOP 2010. LNCS, vol. 6012. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6

    Book  Google Scholar 

  22. Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2–3), 202–220 (2009)

    Article  MathSciNet  Google Scholar 

  23. Huang, X., Wang, J., Qiao, J., Zheng, L., Zhang, J., Wong, R.K.: Performance and replica consistency simulation for quorum-based NoSQL system cassandra. In: van der Aalst, W., Best, E. (eds.) PETRI NETS 2017. LNCS, vol. 10258, pp. 78–98. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57861-3_6

    Chapter  Google Scholar 

  24. Ichbiah, J., Barnes, J.G.P., Heliard, J.C., Krieg-Brückner, B., Roubine, O., Wichmann, B.A.: Modules and visibility in the Ada programming language. On the Construction of Programs, pp. 153–192. Cambridge University Press, Cambridge (1980)

    Google Scholar 

  25. Jensen, K., Kristensen, L.M.: Coloured Petri Nets - Modelling and Validation of Concurrent Systems. Springer, Berlin (2009). https://doi.org/10.1007/b95112

    Book  MATH  Google Scholar 

  26. Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_8

    Chapter  Google Scholar 

  27. Johnsen, E.B., Owe, O., Schlatte, R., Tapia Tarifa, S.L.: Dynamic resource reallocation between deployment components. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 646–661. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16901-4_42

    Chapter  Google Scholar 

  28. Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: Modeling resource-aware virtualized applications for the cloud in real-time ABS. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 71–86. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34281-3_8

    Chapter  Google Scholar 

  29. Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: Integrating deployment architectures and resource consumption in timed object-oriented models. J. Log.Al Algebr. Methods Program. 84(1), 67–91 (2015)

    Article  Google Scholar 

  30. Jørgensen, J.B., Mortensen, K.H.: Modelling and analysis of distributed program execution in BETA using coloured petri nets. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 249–268. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61363-3_14

    Chapter  Google Scholar 

  31. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)

    Article  Google Scholar 

  32. Long, B., Strooper, P.A., Wildman, L.: A method for verifying concurrent Java components based on an analysis of concurrency failures. Concurr. Comput.: Pract. Exp. 19(3), 281–294 (2007)

    Article  Google Scholar 

  33. Reisig, W., Rozenberg, G. (eds.): Lectures on Petri Nets I: Basic Models - Advances in Petri Nets. Springer, Berlin (1998). https://doi.org/10.1007/3-540-65306-6

    MATH  Google Scholar 

  34. Shao, Z., Pierce, B.C. (eds.): Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009. ACM (2009)

    Google Scholar 

  35. Wells, L., Christensen, S., Kristensen, L.M., Mortensen, K.H.: Simulation based performance analysis of web servers. In: Proceedings of PNPM’01, pp. 59–68 (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, University of Oslo, Oslo, Norway

    Anastasia Gkolfi, Einar Broch Johnsen & Ingrid Chieh Yu

  2. Western Norway University of Applied Sciences, Bergen, Norway

    Lars Michael Kristensen

Authors
  1. Anastasia Gkolfi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Einar Broch Johnsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lars Michael Kristensen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ingrid Chieh Yu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Anastasia Gkolfi , Einar Broch Johnsen , Lars Michael Kristensen or Ingrid Chieh Yu .

Editor information

Editors and Affiliations

  1. Pohang University of Science and Technology, Pohang, Korea (Republic of)

    Kyungmin Bae

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

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

Gkolfi, A., Johnsen, E.B., Kristensen, L.M., Yu, I.C. (2018). Using Coloured Petri Nets for Resource Analysis of Active Objects. In: Bae, K., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2018. Lecture Notes in Computer Science(), vol 11222. Springer, Cham. https://doi.org/10.1007/978-3-030-02146-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02146-7_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02145-0

  • Online ISBN: 978-3-030-02146-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation