Programming and verifying component ensembles. (English) Zbl 1416.68051
Bensalem, Saddek (ed.) et al., From programs to systems. The systems perspective in computing. ETAPS workshop, FPS 2014, in honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8415, 69-83 (2014).
Summary: A simplified version of the kernel language SCEL, that we call SCELlight, is introduced as a formalism for programming and verifying properties of so-called cyber-physical systems consisting of software-intensive ensembles of components, featuring complex intercommunications and interactions with humans and other systems. In order to validate the amenability of the language for verification purposes, we provide a translation of SCELlight specifications into Promela. We test the feasibility of the approach by formally specifying an application scenario, consisting of a collection of components offering a variety of services meeting different quality levels, and by using SPIN to verify that some desired behaviors are guaranteed.
For the entire collection see [Zbl 1291.68012].
For the entire collection see [Zbl 1291.68012].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Keywords:
cyber-physical systems; component-based systems; formal methods; process calculi; verification; model checkingReferences:
| [1] | Project InterLink (2007), http://interlink.ics.forth.gr |
| [2] | Sommerville, I., Cliff, D., Calinescu, R., Keen, J., Kelly, T., Kwiatkowska, M.Z., McDermid, J.A., Paige, R.F.: Large-scale complex IT systems. Commun. ACM 55(7), 71–77 (2012) · doi:10.1145/2209249.2209268 |
| [3] | De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL Language. ACM Transactions on Autonomous and Adaptive Systems (to appear, 2014), available as Technical Report from http://eprints.imtlucca.it/2117/ |
| [4] | Cesari, L., De Nicola, R., Pugliese, R., Puviani, M., Tiezzi, F., Zambonelli, F.: Formalising Adaptation Patterns for Autonomic Ensembles. In: Proc. of the 10th International Symposium on Formal Aspects of Component Software (FACS 2013). LNCS, Springer, Heidelberg (2014) |
| [5] | De Nicola, R., Ferrari, G., Loreti, M., Pugliese, R.: A Language-Based Approach to Autonomic Computing. In: Beckert, B., Damiani, F., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2011. LNCS, vol. 7542, pp. 25–48. Springer, Heidelberg (2012), http://rap.dsi.unifi.it/scel/ |
| [6] | Margheri, A., Pugliese, R., Tiezzi, F.: Linguistic Abstractions for Programming and Policing Autonomic Computing Systems. In: Proc. of the 10th IEEE International Conference on Autonomic and Trusted Computing (ATC 2013). IEEE Computer Society (2014) |
| [7] | Mayer, P., Klarl, A., Hennicker, R., Puviani, M., Tiezzi, F., Pugliese, R., Keznikl, J., Bures, T.: The Autonomic Cloud: A vision of voluntary, peer-2-peer cloud computing. In: Proc. of the 2013 IEEE Seventh International Conference on Self-Adaptive and Self-Organizing Systems Workshops (SASOW 2013). IEEE Computer Society (2014) |
| [8] | Bures, T., De Nicola, R., Gerostathopoulos, I., Hoch, N., Kit, M., Koch, N., Monreale, G., Montanari, U., Pugliese, R., Serbedzija, N., Wirsing, M., Zambonelli, F.: A Life Cycle for the Development of Autonomic Systems: The e-mobility showcase. In: Proc. of the 2013 IEEE Seventh International Conference on Self-Adaptive and Self-Organizing Systems Workshops (SASOW 2013). IEEE Computer Society (2014) |
| [9] | Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997) · doi:10.1109/32.588521 |
| [10] | De Nicola, R., Ferrari, G., Pugliese, R.: Klaim: A Kernel Language for Agents Interaction and Mobility. IEEE Trans. Software Eng. 24(5), 315–330 (1998) · doi:10.1109/32.685256 |
| [11] | ASCENS: Autonomic service-component ensembles, http://www.ascens-ist.eu/ |
| [12] | Belzner, L., De Nicola, R., Vandin, A., Wirsing, M.: Reasoning (on) Service Component Ensembles in Rewriting Logic. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software: A Festschrift Symposium in Honor of Kokichi Futatsugi, SAS 2014 (to appear, April 2014) |
| [13] | jRESP, http://code.google.com/p/jresp/ |
| [14] | Xtext, http://www.eclipse.org/Xtext/ |
| [15] | Demartini, C., Iosif, R., Sisto, R.: dSPIN: A Dynamic Extension of SPIN. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 261–276. Springer, Heidelberg (1999) · doi:10.1007/3-540-48234-2_20 |
| [16] | Iosif, R.: Symmetry reductions for model checking of concurrent dynamic software. STTT 6(4), 302–319 (2004) · doi:10.1007/s10009-004-0154-9 |
| [17] | Bozga, M., Jaber, M., Maris, N., Sifakis, J.: Modeling Dynamic Architectures Using Dy-BIP. In: Gschwind, T., De Paoli, F., Gruhn, V., Book, M. (eds.) SC 2012. LNCS, vol. 7306, pp. 1–16. Springer, Heidelberg (2012) · doi:10.1007/978-3-642-30564-1_1 |
| [18] | Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Software 28(3), 41–48 (2011) · doi:10.1109/MS.2011.27 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
