Skip to main content
SpringerLink
Log in

Modeling and Analyzing Resource-Sensitive Actors: A Tutorial Introduction

  • Conference paper
  • First Online:
Coordination Models and Languages (COORDINATION 2021)

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

Included in the following conference series:

Abstract

Actor languages decouple communication from synchronization, which makes them suitable for distributed and scalable applications with flexible synchronization patterns, but also facilitates analysis. ABS is a timed actor-based modeling language which supports cooperative scheduling and the specification of timing- and resource-sensitive behavior. Cooperative scheduling allows a process which is executing in an actor to be suspended while it is waiting for an event to occur, such that another process in the same actor can execute. Timed semantics allows the specification of the temporal behavior of the modeled system. Resource-sensitive behavior takes a supply and demand perspective of execution, relating cost centers which provision resources to processes which require them. These modeling concepts have been used in ABS to model cloud computing, e.g., data-processing applications running on the Hadoop platform and micro-services running on containers orchestrated by Kubernetes. In this tutorial, we present ABS and its execution environment, and discuss the use of cooperative scheduling and resources in modeling cyber-physical systems and applications deployed on virtualized infrastructure.

This research is supported by the Research Council of Norway via the SIRIUS research center (Grant 237898).

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

Notes

  1. 1.

    https://www.compugene.tu-darmstadt.de.

  2. 2.

    https://www.docker.com/products/docker-desktop.

References

  1. ABS Development Team: ABS Documentation. Version 1.9.2. https://abs-models.org/manual/

  2. Albert, E., et al.: SACO: static analyzer for concurrent objects. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 562–567. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_46

    Chapter  Google Scholar 

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

    Google Scholar 

  4. Albert, E., Gómez-Zamalloa, M., Isabel, M.: SYCO: a systematic testing tool for concurrent objects. In: CC, pp. 269–270. ACM (2016)

    Google Scholar 

  5. Albert, E., Gómez-Zamalloa, M., Isabel, M., Rubio, A., Sammartino, M., Silva, A.: Actor-based model checking for software-defined networks. J. Log. Algebraic Methods Program. 118, 100617 (2021)

    Article  MathSciNet  Google Scholar 

  6. Bezirgiannis, N., de Boer, F., de Gouw, S.: Human-in-the-loop simulation of cloud services. In: De Paoli, F., Schulte, S., Broch Johnsen, E. (eds.) ESOCC 2017. LNCS, vol. 10465, pp. 143–158. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67262-5_11

    Chapter  Google Scholar 

  7. Bezirgiannis, N., de Boer, F., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: Implementing SOS with active objects: a case study of a multicore memory system. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 332–350. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_20

    Chapter  Google Scholar 

  8. Bijo, S., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: A formal model of data access for multicore architectures with multilevel caches. Sci. Comput. Program. 179, 24–53 (2019)

    Article  Google Scholar 

  9. 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 

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

    Google Scholar 

  11. Clarke, D., Muschevici, R., Proença, J., Schaefer, I., Schlatte, R.: Variability modelling in the ABS language. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 204–224. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_11

    Chapter  Google Scholar 

  12. Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. Commun. ACM 51(1), 107–113 (2008)

    Article  Google Scholar 

  13. 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 

  14. Din, C.C., Tapia Tarifa, S.L., Hähnle, R., Johnsen, E.B.: History-based specification and verification of scalable concurrent and distributed systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 217–233. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25423-4_14

    Chapter  Google Scholar 

  15. Doménech, J., Genaim, S., Johnsen, E.B., Schlatte, R.: EasyInterface: a toolkit for rapid development of GUIs for research prototype tools. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 379–383. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54494-5_22

    Chapter  Google Scholar 

  16. de Gouw, S., Mauro, J., Nobakht, B., Zavattaro, G.: Declarative elasticity in ABS. In: Aiello, M., Johnsen, E.B., Dustdar, S., Georgievski, I. (eds.) ESOCC 2016. LNCS, vol. 9846, pp. 118–134. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-44482-6_8

    Chapter  Google Scholar 

  17. Hähnle, R.: The abstract behavioral specification language: a tutorial introduction. In: Giachino, E., Hähnle, R., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 1–37. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40615-7_1

    Chapter  Google Scholar 

  18. Hightower, K., Burns, B., Beda, J.: Kubernetes: Up and Running Dive into the Future of Infrastructure. O’Reilly (2017)

    Google Scholar 

  19. 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 

  20. Johnsen, E.B., Lin, J.-C., Yu, I.C.: Comparing AWS deployments using model-based predictions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 482–496. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_39

    Chapter  Google Scholar 

  21. 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 

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

    Article  Google Scholar 

  23. Kamburjan, E.: Detecting deadlocks in formal system models with condition synchronization. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 76, (2018)

    Google Scholar 

  24. Kamburjan, E., Hähnle, R., Schön, S.: Formal modeling and analysis of railway operations with active objects. Sci. Comput. Program. 166, 167–193 (2018)

    Article  Google Scholar 

  25. Kamburjan, E., Scaletta, M., Rollshausen, N.: Crowbar: behavioral symbolic execution for deductive verification of active objects. CoRR abs/2102.10127 (2021)

    Google Scholar 

  26. Kamburjan, E., Stromberg, J.: Tool support for validation of formal system models: interactive visualization and requirements traceability. In: F-IDE@FM, EPTCS, vol. 310, pp. 70–85 (2019)

    Google Scholar 

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

    Article  Google Scholar 

  28. Lin, J., Lee, M., Yu, I.C., Johnsen, E.B.: A configurable and executable model of Spark Streaming on Apache YARN. Int. J. Grid Util. Comput. 11(2), 185–195 (2020)

    Article  Google Scholar 

  29. Lin, J.C., Mauro, J., Røst, T.B., Yu, I.C.: A model-based scalability optimization methodology for cloud applications. In: IEEE SC2, pp. 163–170. IEEE Computer Society (2017)

    Google Scholar 

  30. Lin, J.-C., Yu, I.C., Johnsen, E.B., Lee, M.-C.: ABS-YARN: a formal framework for modeling Hadoop YARN clusters. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 49–65. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_4

    Chapter  Google Scholar 

  31. Turin, G., Borgarelli, A., Donetti, S., Johnsen, E.B., Tapia Tarifa, S.L., Damiani, F.: A formal model of the Kubernetes container framework. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 558–577. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-61362-4_32

    Chapter  Google Scholar 

  32. Tveito, L., Johnsen, E.B., Schlatte, R.: Global reproducibility through local control for distributed active objects. FASE 2020. LNCS, vol. 12076, pp. 140–160. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45234-6_7

    Chapter  Google Scholar 

  33. Wasser, N., Tabar, A.H., Hähnle, R.: Automated model extraction: from non-deterministic C code to active objects. Sci. Comput. Program. 204, 102597 (2021)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oslo, Oslo, Norway

    Rudolf Schlatte, Einar Broch Johnsen, Eduard Kamburjan & Silvia Lizeth Tapia Tarifa

Authors
  1. Rudolf Schlatte
    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. Eduard Kamburjan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Silvia Lizeth Tapia Tarifa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rudolf Schlatte .

Editor information

Editors and Affiliations

  1. University of Turin, Turin, Italy

    Ferruccio Damiani

  2. Sir Alwyn William Building, University of Glasgow, Glasgow, UK

    Ornela Dardha

A Installing the ABS Compiler

A Installing the ABS Compiler

The ABS compiler is contained in a file absfrontend.jar; the latest released version can be found at https://github.com/abstools/abstools/releases/latest. To run the compiler and the generated models, a Java development kit (JDK) version 11 or greater, and Erlang version 22 or greater must be installed.

Then, to compile an ABS file model.abs, use the command java -jar absfrond.jar –erlang model.abs. The compiler creates a subdirectory gen/, the compiled model can be run with the command gen/erl/run (or, on Windows, gen/erl/run.bat).

More detailed installation instructions, including links to the necessary software, is at https://abs-models.org/getting_started/local-install/.

Models that do not use the Model API can also be written and run in a web-based IDE based on EasyInterface [15]. To run the collaboratory locally, install dockerFootnote 2 then run the following command: docker run -d –rm -p 8080:80 –name collaboratory abslang/collaboratory:latest and connect a browser to http://localhost:8080/. On the start page, you can access ABS documentation and examples, and go to the web-based IDE. To shut down the collaboratory, run the command docker stop collaboratory.

Rights and permissions

Reprints and permissions

Copyright information

© 2021 IFIP International Federation for Information Processing

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Schlatte, R., Johnsen, E.B., Kamburjan, E., Tapia Tarifa, S.L. (2021). Modeling and Analyzing Resource-Sensitive Actors: A Tutorial Introduction. In: Damiani, F., Dardha, O. (eds) Coordination Models and Languages. COORDINATION 2021. Lecture Notes in Computer Science(), vol 12717. Springer, Cham. https://doi.org/10.1007/978-3-030-78142-2_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-78142-2_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-78141-5

  • Online ISBN: 978-3-030-78142-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation