Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Empirical Software Engineering Models: Can They Become the Equivalent of Physical Laws in Traditional Engineering? Kapitel lesen Erstes Kapitel lesen

2013 | OriginalPaper | Buchkapitel

Towards Agile Verification

verfasst von : Carlo Ghezzi, Amir Molzam Sharifloo, Claudio Menghi

Erschienen in: Perspectives on the Future of Software Engineering

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

Advances in software verification techniques have been impressive in the past decade. Formal verification of large production software is now increasingly feasible and this is paving the way to transferring these techniques from research to practice. We argue, however, that there is still a serious mismatch between verification and modern development processes, which highly focus on agility and incremental, iterative development. To address this issue, verification has to become agile, and seamless introduction into agile processes has to become feasible. We envision new approaches that will support verification-driven development in the same way as test-driven development is possible today, for example through JUnit within an IDE like Eclipse. In this paper we discuss how agile verification can be achieved, and we show some promising initial steps in this direction.

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 Domain Modeling and Domain Engineering: Key Tasks in Requirements Engineering
Nächstes Kapitel On Model-Based Software Development
Fußnoten
1
The sum of the execution probabilities of the alternative behaviors shall equal to one.
 
2
For both SDs and MCs it is possible to also support hierarchical decompositions, where an SC message OR a MC transition is detailed by a sub-SC or a sub-MC, respectively. This is ignored here for the sake of simplicity.
 
3
For a discussion of qualitative versus quantitative verification, please refer to [23].
 
4
Note that in Fig. 4a we use a logarithmic scale.
 
5
Figure 4a shows linear growth on a logaritmic scale because the number of refined states grows exponentially with the number of levels.
 
Literatur
1.
Baier, C., Katoen, J.-P.: Principles of Model Checking, vol. 26202649. MIT, Cambridge (2008)MATH
2.
Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D.: A syntactic-semantic approach to incremental verification. In: Submitted for Publication (2013)
3.
Breu, R., Hinkel, U., Hofmann, C., Klein, C., Paech, B., Rumpe, B., Thurner, V.: Towards a formalization of the unified modeling language. In: Aksit, M., Matsuoka, S. (eds.) ECOOP’97 Object-Oriented Programming, Jyväskylä. Lecture Notes in Computer Science, vol. 1241, pp. 344–366. Springer, Berlin/Heidelberg (1997)CrossRef
4.
Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69–77 (2012)CrossRef
5.
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT, Cambridge (2000)
6.
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’03, Warsaw, 2003, pp. 331–346
7.
Cordy, M., Schobbens, P.-Y., Heymans, P., Legay, A.: Towards an incremental automata-based approach for software product-line model checking. In: Proceedings of the 16th International Software Product Line Conference—Volume 2, SPLC ’12, Salvador, 2012, pp. 74–81
8.
Famelis, M., Salay, R., Chechik, M.: Partial models: towards modeling and reasoning with uncertainty. In: 34th International Conference on Software Engineering (ICSE), Zurich, June 2012, pp. 573–583
9.
Filieri, A., Ghezzi, C.: Further steps towards efficient runtime verification: handling probabilistic cost models. In: 2012 Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA), Zurich, pp. 2–8. IEEE (2012)
10.
Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: Proceedings of the 33rd International Conference on Software Engineering, Waikiki, Honolulu, pp. 341–350. ACM (2011)
11.
Fisler, K., Krishnamurthi, S.: Modular verification of collaboration-based software designs. In: Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-9, Vienna, pp. 152–163. ACM, New York (2001)
12.
Flanagan, C., Qadeer, S.: Assume-guarantee model checking. Technical report, Microsft Research (2003)
13.
Fowler, M., Highsmith, J.: The agile manifesto. Softw. Dev. 9(8), 28–35 (2001)
14.
Genest, B., Muscholl, A., Peled, D.: Message sequence charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. Lecture Notes in Computer Science, vol. 3098, pp. 537–558. Springer, Berlin/Heidelberg (2004)CrossRef
15.
Ghezzi, C.: Evolution, adaptation, and the quest for incrementality. In: Monterey Workshop, Oxford, 2012, pp. 369–379
16.
Ghezzi, C., Sharifloo, A.M.: Model-based verification of quantitative non-functional properties for software product lines. Inf. Softw. Technol. 55(3), 508–524 (2013)CrossRef
17.
Ghezzi, C., Menghi, C., Sharifloo, A.M., Spoletini, P.: On requirements verification of evolving models. In: Submitted for publication (2013)
18.
Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering, ASE ’02, Edinburgh, 2002
19.
20.
Henzinger, T., Qadeer, S., Rajamani, S.: You assume, we guarantee: methodology and case studies. In: Hu, A., Vardi, M. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 1427, pp. 440–451. Springer, Berlin/Heidelberg (1998)CrossRef
21.
Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice, pp. 180–181. Springer, Berlin/London (2004)
22.
23.
Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering, Dubrovnik, pp. 449–458. ACM (2007)
24.
Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for Performance Evaluation, pp. 220–270. Springer, Berlin/New York (2007)CrossRef
25.
Kwiatkowska, M., Norman, G., Parker, D.: Prism: probabilistic model checking for performance and reliability analysis. ACM Perform. Eval. Rev. 36(4), 40–45 (2009)CrossRef
26.
Lauterburg, S., Sobeih, A., Marinov, D., Viswanathan, M.: Incremental state-space exploration for programs with dynamically allocated data. In: Proceedings of the 30th International Conference on Software Engineering, Leipzig, pp. 291–300. ACM (2008)
27.
Păsăreanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of software: a comparative case study. In: Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, Trento/Toulouse, 1999, pp. 168–183
28.
Salay, R., Chechik, M., Horkoff, J.: Managing requirements uncertainty with partial models. In: 20th IEEE International Requirements Engineering Conference (RE), Chicago, Sept 2012, pp. 1–10
29.
Sharifloo, A.M., Spoletini, P.: Lover: light-weight formal verification of adaptive systems at run time. In: 9th International Symposium on Formal Aspects of Component Software, Mountain View, 2012, pp. 170–187
30.
Thang, N.T., Katayama, T.: Towards a sound modular model checking of collaboration-based software designs. In: Tenth Asia-Pacific Software Engineering Conference, Chiang Mai, Dec 2003, pp. 88–97
31.
Van Lamsweerde, A.: Requirements Engineering: From System Goals to UML Models to Software Specifications. Wiley, Chichester (2009)
32.
Yang, G., Dwyer, M.B., Rothermel, G.: Regression model checking. In: IEEE International Conference on Software Maintenance, 2009. ICSM 2009, Edmonton, pp. 115–124. IEEE (2009)
33.
Young, M., Pezze, M.: Software Testing and Analysis: Process, Principles, and Techniques. Wiley, Hoboken (2008)
Metadaten
Titel
Towards Agile Verification
verfasst von
Carlo Ghezzi
Amir Molzam Sharifloo
Claudio Menghi
Copyright-Jahr
2013
Verlag
Springer Berlin Heidelberg
Buch
Perspectives on the Future of Software Engineering

Print ISBN: 978-3-642-37394-7

Electronic ISBN: 978-3-642-37395-4

Copyright-Jahr: 2013

DOI
https://doi.org/10.1007/978-3-642-37395-4_3