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.
Keywords
References
Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)
ActorFoundry. http://osl.cs.illinois.edu/software/actor-foundry/
Ren, S., Agha, G., Saito, M.: A modular approach for programming distributed real time systems. J. Parallel Distrib. Comput. 36, 4–12 (1996)
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)
Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: the Rebeca experience. In: Formal Modeling: Actors, Open Systems, Biological Systems (2011)
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)
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)
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)
Larsen, K.G., Legay, A.: On the power of statistical model checking. In: Proceedings of 7th International Symposium, ISoLA 2016, pp. 843–862 (2016)
Bellifemine, F., Caire, G., Greenwood, D.: Developing Multi-agent Systems with JADE. Wiley, Hoboken (2007)
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)
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)
Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60–87 (1990)
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)
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)
Plasma Lab. https://project.inria.fr/plasma-lab/
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)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)