Skip to main content

Modelling and Analysis of Distributed Asynchronous Actor Systems Using Theatre

  • Conference paper
  • First Online:
Cybernetics Approaches in Intelligent Systems (CoMeSySo 2017)

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 661))

Included in the following conference series:

  • 937 Accesses

Abstract

This paper introduces Theatre, a modular software architecture whose aim is supporting modelling, analysis, design and implementation of distributed asynchronous probabilistic and timed/untimed actor systems. A key factor of Theatre is that a same model can be transitioned without distortions from a development phase to the next one. The analysis phase is currently based on the Uppaal Statistical Model Checker (SMC) which automatizes simulations, and uses statistical techniques (e.g., Monte Carlo-like and sequential hypothesis testing) to infer quantitative measures from the simulation runs. The design and implementation phases are based on Java. The paper describes the abstract modelling language of Theatre and focusses on its translation to Uppaal SMC. The approach is practically demonstrated by two modelling examples and their experimental analysis.

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

Access this chapter

Institutional subscriptions

References

  1. Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)

    Google Scholar 

  2. ActorFoundry. http://osl.cs.illinois.edu/software/actor-foundry/

  3. Ren, S., Agha, G., Saito, M.: A modular approach for programming distributed real time systems. J. Parallel Distrib. Comput. 36, 4–12 (1996)

    Article  Google Scholar 

  4. Nigro, L., Pupo, F.: Schedulability analysis of real time actors systems using colored petri nets. In: Agha, G., De Cindio, F., Rozenberg, G. (eds.) Proceedings of Concurrent Object-Oriented Programming and Petri Nets-Advances in Petri Nets. LNCS, vol. 2001, pp. 493–513. Springer, New York (2001)

    Chapter  Google Scholar 

  5. Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: the Rebeca experience. In: Formal Modeling: Actors, Open Systems, Biological Systems (2011)

    Google Scholar 

  6. Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H., Cimini, M.: PTRebeca: modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program. 128, 22–50 (2016)

    Article  Google Scholar 

  7. Jafari, A., Kristinsson, H., Khamespanah, E., Sirjani, M., Magnusson, B.: Statistical model checking of timed rebeca models. Comput. Lang. Syst. Struct. 45, 53–79 (2016)

    Google Scholar 

  8. Younes, H.L.S., Kwiatkowska, M., Normaln, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transf. 8(3), 216–228 (2006)

    Article  Google Scholar 

  9. Larsen, K.G., Legay, A.: On the power of statistical model checking. In: Proceedings of 7th International Symposium, ISoLA 2016, pp. 843–862 (2016)

    Google Scholar 

  10. Bellifemine, F., Caire, G., Greenwood, D.: Developing Multi-agent Systems with JADE. Wiley, Hoboken (2007)

    Book  Google Scholar 

  11. Cicirelli, F., Nigro, L.: Control centric framework for model continuity in time-dependent multi-agent systems. In: Concurrency and Computation: Practice and Experience, vol. 28, pp. 3333–3356. Wiley (2016)

    Google Scholar 

  12. David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMS tutorial. Int. J. Softw. Tools Technol. Transf. 17, 1–19 (2015)

    Article  Google Scholar 

  13. Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60–87 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  14. Varshosaz, M., Khosravi, R.: Modelling and verification of probabilistic actor systems using PRebeca. In: Proceedings of Formal Methods and Software Engineering, FMSE 2012. LNCS, vol. 7635, pp. 135–150. Springer (2012)

    Google Scholar 

  15. Magnússon, B.: Simulation-based analysis of Timed Rebeca using TepProp and SQL. M.Sc. Research thesis, School of Computer Science, Reykjavík University (2012)

    Google Scholar 

  16. Plasma Lab. https://project.inria.fr/plasma-lab/

  17. Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Proceedings of 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer (2006)

    Google Scholar 

  18. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Libero Nigro .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Cite this paper

Nigro, L., Sciammarella, P.F. (2018). Modelling and Analysis of Distributed Asynchronous Actor Systems Using Theatre . In: Silhavy, R., Silhavy, P., Prokopova, Z. (eds) Cybernetics Approaches in Intelligent Systems. CoMeSySo 2017. Advances in Intelligent Systems and Computing, vol 661. Springer, Cham. https://doi.org/10.1007/978-3-319-67618-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67618-0_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67617-3

  • Online ISBN: 978-3-319-67618-0

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics