Abstract
Programming autonomic systems with massive number of heterogeneous components poses a number of challenges to language designers and software engineers and requires the integration of computational tools and reasoning tools. We present a general methodology to enrich SCEL, a recently introduced language for programming systems with massive numbers of components, with reasoning capabilities that are guaranteed by external reasoners. We show how the methodology can be instantiated by considering the Maude implementation of SCEL and a specific reasoner, Pirlo, implemented in Maude as well. Moreover we show how the actual integration can benefit from the existing analytical tools of the Maude framework. In particular, we demonstrate our approach by considering a simple scenario consisting of a group of robots moving in an arena aiming at minimising the number of collisions.
Research supported by the European Integrated Project 257414 ASCENS and by the MIUR COFIN Project CINA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Agha, G.A., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. In: Cerone, A., Wiklicky, H. (eds.) QAPL 2005. ENTCS, vol. 153(2), pp. 213–239. Elsevier (2006)
AlTurki, M., Meseguer, J.: PVeStA: A parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011)
ASCENS Autonomic Service-Component ENSembles, http://www.ascens-ist.eu
Beckert, B., Damiani, F., de Boer, F.S., Bonsangue, M.M. (eds.): FMCO 2011. LNCS, vol. 7542. Springer, Heidelberg (2013)
Belzner, L.: Action programming in rewriting logic (technical communication). Theory and Practice of Logic Programming, On-line Supplement (2013)
Bentea, L., Ölveczky, P.C.: A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing. In: MartÃ-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 77–94. Springer, Heidelberg (2013)
Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.E.: Elan from a rewriting logic point of view. Theor. Comput. Sci. 285(2), 155–185 (2002)
Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: Modelling and analyzing adaptive self-assembly strategies with Maude. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 118–138. Springer, Heidelberg (2012)
Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: A conceptual framework for adaptation. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 240–254. Springer, Heidelberg (2012)
CafeOBJ, http://www.ldl.jaist.ac.jp/cafeobj
Clavel, M., Durán, F., Eker, S., Lincoln, P., MartÃ-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
De Nicola, R., Ferrari, G.L., Loreti, M., Pugliese, R.: A language-based approach to autonomic computing. In: Beckert, et al (eds.) [4], pp. 25–48
De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: SCEL: A language for autonomic computing. Tech. rep. (January 2013), http://rap.dsi.unifi.it/scel/pdf/SCEL-TR.pdf
Diaconescu, R., Futatsugi, K.: CafeOBJ Report. The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol. 6. World Scientific (1998)
Diaconescu, R., Futatsugi, K., Ogata, K.: CafeOBJ: Logical foundations and methodologies. Computers and Artificial Intelligence 22(3-4), 257–283 (2003)
GraphViz – Graph Visualization Software, http://www.graphviz.org
Eckhardt, J., Mühlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 78–93. Springer, Heidelberg (2012)
Hölzl, M., Rauschmayer, A., Wirsing, M.: Software engineering for ensembles. In: Wirsing, M., Banâtre, J.-P., Hölzl, M., Rauschmayer, A. (eds.) Software-Intensive Systems. LNCS, vol. 5380, pp. 45–63. Springer, Heidelberg (2008)
IBM: An architectural blueprint for autonomic computing. Tech. rep., 3rd edn (June 2005)
Project InterLink (2007), http://interlink.ics.forth.gr
Knapp, A., Wirsing, M.: Specifying an airport with CafeOBJ: A case study. In: 2nd CafeOBJ Workshop, Tokio, Japan (1997)
Knapp, A., Wirsing, M.: An event space-based operational semantics of multi-threaded Java and its formalisation in CafeOBJ. In: 3rd CafeOBJ Workshop, Kanazawa, Japan (1998)
Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 1–36. Springer, Heidelberg (2002)
MESSI Maude Ensemble Strategies Simulator and Inquirer (2012), http://sysma.lab.imtlucca.it/tools/ensembles
Pianini, D., Sebastio, S., Vandin, A.: Statistical analysis of chemical computational systems with MultiVeStA and Alchemist, http://eprints.imtlucca.it/1697
Sebastio, S., Vandin, A.: MultiVeStA: Statistical Model Checking for Discrete Event Simulators. In: 7th International Conference on Performance Evaluation Methodologies and Tools (ValueTools 2013), http://eprints.imtlucca.it/1798 , doi:10.4108/icst.valuetools.2013.254377
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)
Sen, K., Viswanathan, M., Agha, G.A.: Vesta: A statistical model-checker and analyzer for probabilistic systems. In: Baier, C., Chiola, G., Smirni, E. (eds.) QEST 2005, pp. 251–252. IEEE Computer Society (2005)
Talcott, C.L.: Coordination models based on a formal model of distributed object reflection. In: Brim, L., Linden, I. (eds.) MTCoord 2005. ENTCS, vol. 150(1), pp. 143–157. Elsevier (2006)
Talcott, C.L.: Policy-based coordination in PAGODA: A case study. In: Boella, G., Dastani, M., Omicini, A., van der Torre, L.W., Cerna, I., Linden, I. (eds.) CoOrg 2006 & MTCoord 2006. ENTCS, vol. 181, pp. 97–112. Elsevier (2007)
Wirsing, M., Hölzl, M.M., Tribastone, M., Zambonelli, F.: Ascens: Engineering autonomic service-component ensembles. In: Beckert, et al. (eds.) [4], pp. 1–24
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Belzner, L., De Nicola, R., Vandin, A., Wirsing, M. (2014). Reasoning (on) Service Component Ensembles in Rewriting Logic. In: Iida, S., Meseguer, J., Ogata, K. (eds) Specification, Algebra, and Software. Lecture Notes in Computer Science, vol 8373. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54624-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-54624-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54623-5
Online ISBN: 978-3-642-54624-2
eBook Packages: Computer ScienceComputer Science (R0)