Model-checking Helena ensembles with Spin. (English) Zbl 1321.68346
Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 331-360 (2015).
Summary: The Helena approach allows to specify dynamically evolving ensembles of collaborating components. It is centered around the notion of roles which components can adopt in ensembles. In this paper, we focus on the early verification of Helena models. We propose to translate Helena specifications into Promela and check satisfaction of LTL properties with Spin [G. Holzmann, The Spin model checker. Reading, MA: Addison-Wesley (2003)]. To prove the correctness of the translation, we consider an SOS semantics of (simplified variants of) Helena and Promela and establish stutter trace equivalence between them. Thus, we can guarantee that a Helena specification and its Promela translation satisfy the same LTL formulae (without next). Our correctness proof relies on a new, general criterion for stutter trace equivalence.
For the entire collection see [Zbl 1319.68011].
For the entire collection see [Zbl 1319.68011].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Baier, C.; Katoen, J., Principles of Model Checking (2008), Cambridge: MIT Press, Cambridge · Zbl 1179.68076 |
| [2] | Boronat, A.; Knapp, A.; Meseguer, J.; Wirsing, M.; Corradini, A.; Montanari, U., What is a multi-modeling language?, Recent Trends in Algebraic Development Techniques, 71-87 (2009), Heidelberg: Springer, Heidelberg · Zbl 1253.68225 · doi:10.1007/978-3-642-03429-9_6 |
| [3] | Bures, T.; Gerostathopoulos, I.; Hnetynka, P.; Keznikl, J.; Kit, M.; Plasil, F.; Wirsing, M.; Hölzl, M.; Koch, N.; Mayer, P., The Invariant Refinement Method, Software Engineering for Collective Autonomic Systems, 405-428 (2015), Switzerland: Springer, Switzerland |
| [4] | Combaz, J.; Bensalem, S.; Kofron, J.; Wirsing, M.; Hölzl, M.; Koch, N.; Mayer, P., Correctness of service components and service component ensembles, Software Engineering for Collective Autonomic Systems, 107-159 (2015), Switzerland: Springer, Switzerland |
| [5] | De Nicola, R.; Lluch Lafuente, A.; Loreti, M.; Morichetta, A.; Pugliese, R.; Senni, V.; Tiezzi, F.; Bensalem, S.; Lakhneck, Y.; Legay, A., Programming and Verifying Component Ensembles, From Programs to Systems, 69-83 (2014), Heidelberg: Springer, Heidelberg · Zbl 1416.68051 |
| [6] | Eckhardt, J.; Mühlbauer, T.; AlTurki, M.; Meseguer, J.; Wirsing, M.; Lara, J.; Zisman, A., Stable availability under denial of service attacks through formal patterns, Fundamental Approaches to Software Engineering, 78-93 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-28872-2_6 |
| [7] | Eckhardt, J.; Mühlbauer, T.; Meseguer, J.; Wirsing, M., Semantics, distributed implementation, and formal analysis of KLAIM models in Maude, Sci. Comput. Program., 99, 24-74 (2015) · doi:10.1016/j.scico.2014.10.001 |
| [8] | Goguen, JA; Meseguer, J.; Nielsen, M.; Schmidt, EM, Universal realization, persistent interconnection and implementation of abstract modules, Automata, Languages and Programming, 265-281 (1982), Heidelberg: Springer, Heidelberg · Zbl 0493.68014 · doi:10.1007/BFb0012775 |
| [9] | Havelund, K.; Larsen, KG; Lingas, K.; Karlsson, R.; Carlsson, S., The fork calculus, Automata, Languages and Programming, 544-557 (1993), Heidelberg: Springer, Heidelberg · Zbl 1418.68142 · doi:10.1007/3-540-56939-1_101 |
| [10] | Hennicker, R.; Klarl, A.; Iida, S.; Meseguer, J.; Ogata, K., Foundations for Ensemble Modeling - The Helena Approach, Specification, Algebra, and Software, 359-381 (2014), Heidelberg: Springer, Heidelberg · Zbl 1320.68118 · doi:10.1007/978-3-642-54624-2_18 |
| [11] | Holzmann, G., The Spin Model Checker (2003), Reading: Addison-Wesley, Reading |
| [12] | Klarl, A.: From helena ensemble specifications to Promela verification models. Technical report, LMU Munich (2015). http://goo.gl/G0sU6U |
| [13] | Klarl, A.; Cichella, L.; Hennicker, R.; Lanese, I.; Madelaine, E., From Helena ensemble specifications to executable code, Formal Aspects of Component Software, 183-190 (2015), Heidelberg: Springer, Heidelberg |
| [14] | Klarl, A., Hennicker, R.: Design and implementation of dynamically evolving ensembles with the helena framework. In: Proceedings of the Australasian Software Engineering Conference, pp. 15-24. IEEE (2014) |
| [15] | Klarl, A.; Mayer, P.; Hennicker, R.; Margaria, T.; Steffen, B., Helena@Work: Modeling the science cloud platform, Leveraging Applications of Formal Methods, Verification and Validation, 99-116 (2014), Heidelberg: Springer, Heidelberg |
| [16] | Lamport, L.: What good is temporal logic? In: IFIP 9th World Congress, pp. 657-668 (1983) |
| [17] | van Lamsweerde, A., Requirements Engineering: from System Goals to UML Models to Software Specifications (2009), New York: Wiley, New York |
| [18] | Magee, J.; Kramer, J., Concurrency-State Models and Java Programs (2006), New York: Wiley, New York · Zbl 0924.68026 |
| [19] | Meseguer, J.; Palomino, M.; Martí-Oliet, N., Algebraic Simulations, J. Logic Algebraic Program., 79, 2, 103-143 (2010) · Zbl 1184.68300 · doi:10.1016/j.jlap.2009.07.003 |
| [20] | Weise, C.: An incremental formal semantics for PROMELA. In: Third SPIN Workshop (1997) |
| [21] | Wirsing, M.; Hölzl, M.; Koch, N.; Mayer, P., Software Engineering for Collective Autonomic Systems (2015), Switzerland: Springer, Switzerland |
| [22] | Wirsing, M.; Knapp, A., A formal approach to object-oriented software engineering, Electr. Notes Theoret. Comput. Sci., 4, 322-360 (1996) · Zbl 1001.68024 · doi:10.1016/S1571-0661(04)00046-5 |
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.
