nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Featured Team Automata

verfasst von : Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença

Erschienen in: Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We propose featured team automata to support variability in the development and analysis of teams, which are systems of reactive components that communicate according to specified synchronisation types. A featured team automaton concisely describes a family of concrete product models for specific configurations determined by feature selection. We focus on the analysis of communication-safety properties, but doing so product-wise quickly becomes impractical. Therefore, we investigate how to lift notions of receptiveness (no message loss) to the level of family models. We show that featured (weak) receptiveness of featured team automata characterises (weak) receptiveness for all product instantiations. A prototypical tool supports the developed theory.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Congruence Relations for Büchi Automata

Nächstes Kapitel From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET

Otherwise, the components in J could simply output a without reception.

Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37521-7CrossRef

Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: Formal description of variability in product families. In: Proceedings of the 15th International Software Product Lines Conference (SPLC), pp. 130–139. IEEE (2011). https://doi.org/10.1109/SPLC.2011.34

Basile, D., et al.: Controller synthesis of service contracts with variability. Sci. Comput. Program. 187, 102344 (2020). https://doi.org/10.1016/j.scico.2019.102344CrossRef

Basile, D., Di Giandomenico, F., Gnesi, S., Degano, P., Ferrari, G.L.: Specifying variability in service contracts. In: Proceedings of the 11th International Workshop on Variability Modelling of Software-Intensive Systems (VaMoS), pp. 20–27. ACM (2017). https://doi.org/10.1145/3023956.3023965

Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175–189. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_15CrossRefMATH

ter Beek, M.H., Carmona, J., Hennicker, R., Kleijn, J.: Communication requirements for team automata. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. LNCS, vol. 10319, pp. 256–277. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59746-1_14CrossRef

ter Beek, M.H., Cledou, G., Hennicker, R., Proença, J.: Featured Team Automata. arXiv:2108.01784 (August 2021)

ter Beek, M.H., Damiani, F., Lienhardt, M., Mazzanti, F., Paolini, L.: Efficient static analysis and verification of featured transition systems. Empir. Softw. Eng. 10 (2021). https://doi.org/10.1007/s10664-020-09930-8

ter Beek, M.H., Ellis, C.A., Kleijn, J., Rozenberg, G.: Synchronizations in team automata for groupware systems. Comput. Sup. Coop. Work 12(1), 21–69 (2003). https://doi.org/10.1023/A:1022407907596CrossRef

10.

ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebr. Methods. Program. 85(2), 287–315 (2016). https://doi.org/10.1016/j.jlamp.2015.11.006MathSciNetCrossRefMATH

11.

ter Beek, M.H., Hennicker, R., Kleijn, J.: Compositionality of safe communication in systems of team automata. In: Pun, V.K.I., Stolz, V., Simao, A. (eds.) ICTAC 2020. LNCS, vol. 12545, pp. 200–220. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-64276-1_11CrossRefMATH

12.

ter Beek, M.H., Kleijn, J.: Modularity for teams of I/O automata. Inf. Process. Lett. 95(5), 487–495 (2005). https://doi.org/10.1016/j.ipl.2005.05.012MathSciNetCrossRefMATH

13.

ter Beek, M.H., van Loo, S., de Vink, E.P., Willemse, T.A.C.: Family-based SPL model checking using parity games with variability. In: FASE 2020. LNCS, vol. 12076, pp. 245–265. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45234-6_12CrossRef

14.

ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Family-based model checking with mCRL2. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 387–405. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54494-5_23CrossRef

15.

Carmona, J., Cortadella, J.: Input/output compatibility of reactive systems. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 360–377. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36126-X_22CrossRef

16.

Carmona, J., Kleijn, J.: Compatibility in a multi-component environment. Theor. Comput. Sci. 484, 1–15 (2013). https://doi.org/10.1016/j.tcs.2013.03.006MathSciNetCrossRefMATH

17.

Češka, M., Jansen, N., Junges, S., Katoen, J.-P.: Shepherding hordes of Markov chains. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019, Part II. LNCS, vol. 11428, pp. 172–190. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_10CrossRef

18.

Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Form. Asp. Comput. 30(1), 45–75 (2017). https://doi.org/10.1007/s00165-017-0432-4MathSciNetCrossRef

19.

Classen, A.: Modelling and Model Checking Variability-Intensive Systems. Ph.D. thesis, University of Namur (2011). http://hdl.handle.net/2078.2/90863

20.

Classen, A., Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069–1089 (2013). https://doi.org/10.1109/TSE.2012.86CrossRef

21.

Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd International Conference on Software Engineering (ICSE), pp. 335–344. ACM (2010). https://doi.org/10.1145/1806799.1806850

22.

Damiani, F., Schaefer, I.: Family-based analysis of type safety for delta-oriented software product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 193–207. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34026-0_15CrossRef

23.

de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE), pp. 109–120. ACM (2001). https://doi.org/10.1145/503209.503226

24.

Dimovski, A.S.: \(\text{ CTL}^{\star }\) family-based model checking using variability abstractions and modal transition systems. Int. J. Softw. Tools Technol. Transf. 22(1), 35–55 (2019). https://doi.org/10.1007/s10009-019-00528-0CrossRef

25.

Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wąsowski, A.: Efficient family-based model checking via variability abstractions. Int. J. Softw. Tools Technol. Transf. 19(5), 585–603 (2016). https://doi.org/10.1007/s10009-016-0425-2CrossRef

26.

Ellis, C.A.: Team automata for groupware systems. In: Proceedings of the 1st International ACM SIGGROUP Conference on Supporting Group Work (GROUP), pp. 415–424. ACM (1997). https://doi.org/10.1145/266838.267363

27.

Fantechi, A., Gnesi, S.: A behavioural model for product families. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE), pp. 521–524. ACM (2007). https://doi.org/10.1145/1287624.1287700

28.

Fischbein, D., Uchitel, S., Braberman, V.A.: A foundation for behavioural conformance in software product line architectures. In: Proceedings of the ISSTA Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA), pp. 39–48. ACM (2006). https://doi.org/10.1145/1147249.1147254

29.

Hennicker, R., Bidoit, M.: Compatibility properties of synchronously and asynchronously communicating components. Log. Methods Comput. Sci. 14(1), 1–31 (2018). https://doi.org/10.23638/LMCS-14(1:1)2018

30.

Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_6CrossRefMATH

31.

Lauenroth, K., Pohl, K., Töhning, S.: Model checking of domain artifacts in product line engineering. In: Proceedings of the 24th International Conference on Automated Software Engineering (ASE), pp. 269–280. IEEE (2009). https://doi.org/10.1109/ASE.2009.16

32.

Liang, J.H., Ganesh, V., Czarnecki, K., Raman, V.: SAT-based Analysis of large real-world feature models is easy. In: Proceedings of the 19th International Software Product Line Conference (SPLC), pp. 91–100. ACM (2015). https://doi.org/10.1145/2791060.2791070

33.

Mendonça, M., Wąsowski, A., Czarnecki, K.: SAT-based analysis of feature models is easy. In: Proceedings of the 13th International Software Product Line Conference (SPLC), pp. 231–240. ACM (2009)

34.

Muschevici, R., Proença, J., Clarke, D.: Feature nets: behavioural modelling of software product lines. Softw. Syst. Model. 15(4), 1181–1206 (2015). https://doi.org/10.1007/s10270-015-0475-zCrossRefMATH

35.

Muschevici, R., Proença, J., Clarke, D.: Modular modelling of software product lines with feature nets. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 318–333. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24690-6_22CrossRefMATH

36.

Schobbens, P., Heymans, P., Trigaux, J.C., Bontemps, Y.: Feature diagrams: a survey and a formal semantics. In: Proceedings of the 14th IEEE International Conference on Requirements Engineering (RE), pp. 136–145. IEEE (2006). https://doi.org/10.1109/RE.2006.23

37.

Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6 (2014). https://doi.org/10.1145/2580950CrossRef

38.

Thüm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering (GPCE), pp. 11–20. ACM (2012). https://doi.org/10.1145/2371401.2371404

Titel: Featured Team Automata
verfasst von: Maurice H. ter Beek
Guillermina Cledou
Rolf Hennicker
José Proença
Verlag: Springer International Publishing
Buch: Formal Methods
Print ISBN: 978-3-030-90869-0

Electronic ISBN: 978-3-030-90870-6

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-90870-6_26

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner