nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Supervisory Controller Synthesis for Product Lines Using CIF 3

verfasst von : Maurice H. ter Beek, Michel A. Reniers, Erik P. de Vink

Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques

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

Using the CIF 3 toolset, we illustrate the general idea of controller synthesis for product line engineering for a prototypical example of a family of coffee machines. The challenge is to integrate a number of given components into a family of products such that the resulting behaviour is guaranteed to respect an attributed feature model as well as additional behavioural requirements. The proposed correctness-by-construction approach incrementally restricts the composed behaviour by subsequently incorporating feature constraints, attribute constraints and temporal constraints. The procedure as presented focusses on synthesis, but leaves ample opportunity to handle e.g. uncontrollable behaviour, dynamic reconfiguration, and product- and family-based analysis.

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 Proof-Carrying Apps: Contract-Based Deployment-Time Verification

Nächstes Kapitel Partial Verification and Intermediate Results as a Solution to Combine Automatic and Interactive Verification Techniques

Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A compositional framework to derive product line behavioural descriptions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 146–161. Springer, Heidelberg (2012)

Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

Ba̧k, K., Diskin, Z., Antkiewicz, M., Czarnecki, K., Wa̧sowski, A.: Clafer: unifying class and feature modeling. Softw. Syst. Model. 15, 811–845 (2015)CrossRef

ter Beek, M.H., de Vink, E.P.: Towards modular verification of software product lines with mCRL2. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 368–385. Springer, Heidelberg (2014)

ter Beek, M.H., de Vink, E.P.: Using mCRL2 for the analysis of software product lines. In: FormaliSE 2014, pp. 31–37. IEEE (2014)

ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Towards a feature mu-Calculus targeting SPL verification. In: FMSPLE 2016, EPTCS, vol. 206, pp. 61–75 (2016)

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)MathSciNetCrossRefMATH

ter Beek, M.H., Legay, A., Lafuente, A.L., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: SPLC 2015, pp. 11–15. ACM (2015)

ter Beek, M.H., Legay, A., Lafuente, A.L., Vandin, A.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 114–133. Springer, Heidelberg (2016)

10.

ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450–454. Springer, Heidelberg (2012)CrossRef

11.

van Beek, D.A., Fokkink, W.J., Hendriks, D., Hofkamp, A., Markovski, J., van de Mortel-Fronczak, J.M., Reniers, M.A.: CIF 3: model-based engineering of supervisory controllers. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 575–580. Springer, Heidelberg (2014)CrossRef

12.

Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST 2006, pp. 125–126. IEEE (2006)

13.

Benavides, D., Segura, S., Ruiz-Cortés, A.: Automated analysis of feature models 20 years later: a literature review. Inf. Syst. 35(6), 615–636 (2010)CrossRef

14.

Bubel, R., Hähnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 120–134. Springer, Heidelberg (2014)

15.

Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y.: Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transfer 14(5), 589–612 (2012)CrossRef

16.

Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80, 416–439 (2014)CrossRef

17.

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. Software Eng. 39(8), 1069–1089 (2013)CrossRef

18.

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: ICSE 2010, pp. 335–344. ACM (2010)

19.

Cordy, M., Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: ProVeLines: a product line of verifiers for software product lines. In: SPLC 2013, vol. 2, pp. 141–146. ACM (2013)

20.

Delaware, B., Cook, W.R., Batory, D.S.: Product lines of theorems. In: Lopes, C.V., Fisher, K., (eds.) OOPSLA 2011, pp. 595–608. ACM (2011)

21.

Dijkstra, E.W.: A constructive approach to the problem of program correctness. BIT Numer. Math. 8(3), 174–186 (1968)MathSciNetCrossRefMATH

22.

Forschelen, S.T.J., van de Mortel-Fronczak, J.M., Su, R., Rooda, J.E.: Application of supervisory control theory to theme park vehicles. Discrete Event Dyn. Syst. 22(4), 511–540 (2012)MathSciNetCrossRefMATH

23.

Gohari, P., Wonham, W.M.: On the complexity of supervisory control design in the RW framework. IEEE Trans. Syst. Man Cybern. 30(5), 643–652 (2000). Part BCrossRef

24.

Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113–131. Springer, Heidelberg (2008)CrossRef

25.

Hähnle, R., Schaefer, I.: A Liskov principle for delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 32–46. Springer, Heidelberg (2012)CrossRef

26.

Hall, A.: Correctness by construction: integrating formality into a commercial development process. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 224–233. Springer, Heidelberg (2002)CrossRef

27.

Hall, A., Chapman, R.: Correctness by construction: developing a commercial secure system. IEEE Softw. 19(1), 18–25 (2002)CrossRef

28.

Hoare, C.A.R.: Proof of a program: FIND. Commun. ACM 14(1), 39–45 (1971)CrossRefMATH

29.

Jackson, D., Abstractions, S.: Logic, Language, and Analysis. MIT Press, Cambridge (2006)

30.

Juodisius, P., Sarkar, A., Mukkamala, R.R., Antkiewicz, M., Czarnecki, K., Wa̧sowski, A.: Clafer: lightweight modeling of structure and behavior with variability. Unpublished manuscript

31.

Lauenroth, K., Pohl, K., Töhning, S.: Model checking of domain artifacts in product line engineering. In: ASE 2009, pp. 269–280. IEEE (2009)

32.

Leucker, M., Thoma, D.: A formal approach to software product families. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 131–145. Springer, Heidelberg (2012)

33.

Lochau, M., Mennicke, S., Baller, H., Ribbeck, L.: DeltaCCS: a core calculus for behavioral change. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 320–335. Springer, Heidelberg (2014)

34.

Mannion, M., Camara, J.: Theorem proving for product line model verification. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 211–224. Springer, Heidelberg (2004)CrossRef

35.

Markovski, J., Jacobs, K.G.M., van Beek, D.A., Somers, L.J.A.M., Rooda, J.E.: Coordination of resources using generalized state-based requirements. In: Raisch, J., Giua, A., Lafortune, S., Moor, T. (eds.) WODES 2010, pp. 287–292. International Federation of Automatic Control (2010)

36.

Ouedraogo, L., Kumar, R., Malik, R., Åkesson, K.: Nonblocking and safe control of discrete-event systems modeled as extended finite automata. IEEE Trans. Autom. Sci. Eng. 8(3), 560–569 (2011)CrossRef

37.

Pohl, K., Böckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, Heidelberg (2005)CrossRefMATH

38.

Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)MathSciNetCrossRefMATH

39.

Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. MIT Press, Cambridge (2001)MATH

40.

Schaefer, I.: Variability modelling for model-driven development of software product lines. In: Benavides, D., Batory, D.S., Grünbacher, P. (eds.) VaMoS 2010, ICB-Research report, vol. 37, pp. 85–92. Universität Duisburg-Essen (2010)

41.

Skoldstam, M., Åkesson, K., Fabian, M.: Modeling of discrete event systems using finite automata with variables. In: CDC 2007, pp. 3387–3392 (2007)

42.

van der Sanden, B., Reniers, M.A., Geilen, M., Basten, T., Jacobs, J., Voeten, J., Schiffelers, R.R.H.: Modular model-based supervisory controller design for wafer logistics in lithography machines. In: MoDELS 2015, pp. 416–425. IEEE (2015)

43.

Swartjes, L., Reniers, M.A., van Beek, D., Fokkink, W.: Why is my supervisor empty? Finding causes for the unreachability of states in synthesized supervisors. In: Cassandras, C.G., Giua, A., Li, Z. (eds.) WODES 2016, pp. 14–21. IEEE (2016)

44.

Theunissen, R.J.M., van Beek, D.A., Rooda, J.E.: Improving evolvability of a patient communication control system using state-based supervisory control synthesis. Adv. Eng. Inform. 26(3), 502–515 (2012)CrossRef

45.

Thüm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: GPCE 2012, pp. 11–20. ACM (2012)

Titel: Supervisory Controller Synthesis for Product Lines Using CIF 3
verfasst von: Maurice H. ter Beek
Michel A. Reniers
Erik P. de Vink
Verlag: Springer International Publishing
Buch: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques
Print ISBN: 978-3-319-47165-5

Electronic ISBN: 978-3-319-47166-2

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-47166-2_59

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"