nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Modularization of Refinement Steps for Agile Formal Methods

verfasst von : Fabian Benduhn, Thomas Thüm, Ina Schaefer, Gunter Saake

Erschienen in: Formal Methods and Software Engineering

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

The combination of agile methods and formal methods has been recognized as a promising field of research. However, many formal methods rely on a refinement-based development process which poses problems for their integration into agile processes. We consider redundancies within refinement hierarchies as a challenge for the practical application of stepwise refinement and propose superimposition-based modularization of refinement steps as a potential solution. While traditionally, each model in a refinement hierarchy must be developed and maintained separately, our concept allows developers to specify the refinement steps that transform a model into a refined one. We have developed tool support for the language AsmetaL and evaluated our approach by means of a case study. The results indicate a reduction of complexity for the development artifacts in terms of their overall size by 48.6% for the ground model and four refinements. Furthermore, the case study shows that superimposition-based refinement eases the development of alternative refinements for exploratory development and to cope with changing requirements. Thus, we consider this work as a step towards agile formal methods that are tailored to support iterative development, facilitating their incorporation into agile development processes.

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 Towards Customizable CPS: Composability, Efficiency and Predictability

Nächstes Kapitel Model Checking Pushdown Epistemic Game Structures

http://asmeta.sourceforge.net/.

Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefMATH

Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006). doi:10.1007/11901433_32 CrossRef

Al-Hajjaji, M., Meinicke, J., Krieter, S., Schröter, R., Thüm, T., Leich, T., Saake, G.: Tool demo: testing configurable systems with featureIDE. In: Proceedings of International Conference on Generative Programming: Concepts and Experiences (GPCE), pp. 173–177. ACM, New York (2016)

Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, Berlin, Heidelberg (2013)CrossRef

Apel, S., Kästner, C., Lengauer, C.: Language-independent and automated software composition: the featurehouse experience. IEEE Trans. Softw. Eng. (TSE) 39(1), 63–79 (2013)CrossRef

Apel, S., von Rhein, A., Thüm, T., Kästner, C.: Feature-interaction detection based on feature-based specifications. Comput. Netw. 57(12), 2399–2409 (2013)CrossRef

Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1–18. Springer, Cham (2014). doi:10.1007/978-3-319-07512-9_1 CrossRef

Arcaini, P., Gargantini, A., Riccobene, E.: Rigorous development process of a safety-critical system: from asm models to java code. Int. J. Softw. Tools Technol. Transfer 19(2), 247–269 (2017)CrossRef

Banach, R.: Model based refinement and the tools of tomorrow. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 42–56. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87603-8_5 CrossRef

10.

Batory, D.: A tutorial on feature oriented programming and the AHEAD tool suite. In: Lämmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2005. LNCS, vol. 4143, pp. 3–35. Springer, Heidelberg (2006). doi:10.1007/11877028_1 CrossRef

11.

Batory, D., Börger, E.: Modularizing theorems for software product lines: the Jbook case study. J. Univ. Comput. Sci. (J.UCS) 14(12), 2059–2082 (2008)

12.

Batory, D., Sarvela, J.N., Rauschmayer, A.: Scaling step-wise refinement. IEEE Trans. Softw. Eng. (TSE) 30(6), 355–371 (2004)CrossRef

13.

Black, S., Boca, P.P., Bowen, J.P., Gorman, J., Hinchey, M.: Formal versus agile: survival of the fittest. Comput. 42(9), 37–45 (2009)CrossRef

14.

15.

Börger, E.: High level system design and analysis using abstract state machines. In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 1–43. Springer, Heidelberg (1999). doi:10.1007/3-540-48257-1_1 CrossRef

16.

Börger, E.: The asm refinement method. Formal Aspects Comput. 15(2), 237–257 (2003)CrossRefMATH

17.

Börger, E., Stark, R.F.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Secaucus (2003)CrossRefMATH

18.

Bougé, L., Francez, N.: A compositional approach to superimposition. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 240–249. ACM (1988)

19.

Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. (CSUR) 28(4), 626–643 (1996)CrossRef

20.

Clifton, C., Leavens, G.T.: Observers and assistants: a proposal for modular aspect-oriented reasoning. In: Proceedings of Workshop Foundations of Aspect-Oriented Languages (FOAL), pp. 33–44. Iowa State University, Ames, April 2002

21.

Dubinsky, Y., Rubin, J., Berger, T., Duszynski, S., Becker, M., Czarnecki, K.: An exploratory study of cloning in industrial software product lines. In: Proceedings of European Conference on Software Maintenance and Reengineering (CSMR), pp. 25–34. IEEE, Washington, DC (2013)

22.

Dubslaff, C., Klüppelholz, S., Baier, C.: Probabilistic model checking for energy analysis in software product lines. In: Proceedings of International Conference on Aspect-Oriented Software Development (AOSD), pp. 169–180. ACM, New York (2014)

23.

Edmunds, A., Olszewska, M., Waldén, M.: Using the event-b formal method for disciplined agile delivery of safety-critical systems (2015)

24.

Eleftherakis, G., Cowling, A.J.: An agile formal development methodology. In: Proceedings of the 1st South-East European Workshop on Formal Methods, pp. 36–47 (2003)

25.

Ernst, G., Pfähler, J., Schellhorn, G., Reif, W.: Modular refinement for submachines of asms. In: Ameur, Y.A., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. LNCS, vol. 8477, pp. 188–203. Springer, Heidelberg (2014). doi:10.1007/978-3-662-43652-3_16 CrossRef

26.

Fiadeiro, J., Maibaum, T.: Categorical semantics of parallel program design. Sci. Comput. Program. 28(2–3), 111–138 (1997)CrossRefMATH

27.

Gargantini, A., Riccobene, E., Scandurra, P.: Deriving a textual notation from a metamodel: an experience on bridging modelware and grammarware. Milestones, Models and Mappings for Model-Driven Architecture, p. 33 (2006)

28.

Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J. UCS 14(12), 1949–1983 (2008)

29.

Gondal, A., Poppleton, M., Butler, M.: Composing event-B specifications - case-study experience. In: Apel, S., Jackson, E. (eds.) SC 2011. LNCS, vol. 6708, pp. 100–115. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22045-6_7 CrossRef

30.

Gurevich, Y.: Sequential abstract-state machines capture sequential algorithms. ACM Trans. Comput. Logic (TOCL) 1(1), 77–111 (2000)MathSciNetCrossRefMATH

31.

Hähnle, R., Schaefer, I.: A Liskov principle for delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 32–46. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34026-0_4 CrossRef

32.

Katz, S.: A superimposition control construct for distributed systems. ACM Trans. Program. Lang. Syst. (TOPLAS) 15(2), 337–356 (1993)CrossRef

33.

Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Akşit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997). doi:10.1007/BFb0053381

34.

Kim, C.H.P., Marinov, D., Khurshid, S., Batory, D., Souto, S., Barros, P., D’Amorim, M.: SPLat: lightweight dynamic analysis for reducing combinatorics in testing configurable systems. In: Proceedings of European Software Engineering Conference/Foundations of Software Engineering (ESEC/FSE), pp. 257–267. ACM, New York, August 2013

35.

Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Heidelberg (2012)CrossRefMATH

36.

Larsen, P.G., Fitzgerald, J.S., Wolff, S.: Are formal methods ready for agility? a reality check. In: FM + AM, pp. 13–25. Citeseer (2010)

37.

Li, H., Krishnamurthi, S., Fisler, K.: Modular verification of open features using three-valued model checking. Autom. Softw. Eng. 12(3), 349–382 (2005)CrossRef

38.

Linsbauer, L., Lopez-Herrejon, R.E., Egyed, A.: Softw. Syst. Model (2016). https://doi.org/10.1007/s10270-015-0512-y

39.

Prehofer, C.: Feature-oriented programming: a fresh look at objects. In: Akşit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 419–443. Springer, Heidelberg (1997). doi:10.1007/BFb0053389

40.

Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (eds.) SPLC 2010. LNCS, vol. 6287, pp. 77–91. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15579-6_6 CrossRef

41.

Schaefer, I., Seidl, C., Cleophas, L.G., Watson, B.W.: Splicing TABASCO: custom-tailored software product line variants from taxonomy-based toolkits. In: SAICSIT 2015, p. 34:1–34:10 (2015)

42.

Spivey, J.M.: Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, New York (1988)MATH

43.

Tarr, P., Ossher, H., Harrison, W., Sutton Jr., S.M.: N degrees of separation: multi-dimensional separation of concerns. In: Proceedings of International Conference on Software Engineering (ICSE), pp. 107–119. ACM, New York (1999)

44.

Thüm, T.: Product-line specification and verification with feature-oriented contracts. Ph.D. thesis, University of Magdeburg, Germany, February 2015

45.

Thüm, T., Kästner, C., Benduhn, F., Meinicke, J., Saake, G., Leich, T.: FeatureIDE: an extensible framework for feature-oriented software development. Sci. Comput. Program. (SCP) 79, 70–85 (2014)CrossRef

46.

Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. (CSUR) 41(4), 19 (2009)CrossRef

47.

Zhao, J., Rinard, M.: Pipa: a behavioral interface specification language for aspect. In: Pezzè, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 150–165. Springer, Heidelberg (2003). doi:10.1007/3-540-36578-8_11 CrossRef

Titel: Modularization of Refinement Steps for Agile Formal Methods
verfasst von: Fabian Benduhn
Thomas Thüm
Ina Schaefer
Gunter Saake
Verlag: Springer International Publishing
Buch: Formal Methods and Software Engineering
Print ISBN: 978-3-319-68689-9

Electronic ISBN: 978-3-319-68690-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-68690-5_2

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