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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 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.
References
Baier, C., Katoen, J.-P.: Principles of Model Checking, vol. 26202649. MIT, Cambridge (2008)
Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D.: A syntactic-semantic approach to incremental verification. In: Submitted for Publication (2013)
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)
Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69–77 (2012)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT, Cambridge (2000)
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
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
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
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)
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)
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)
Flanagan, C., Qadeer, S.: Assume-guarantee model checking. Technical report, Microsft Research (2003)
Fowler, M., Highsmith, J.: The agile manifesto. Softw. Dev. 9(8), 28–35 (2001)
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)
Ghezzi, C.: Evolution, adaptation, and the quest for incrementality. In: Monterey Workshop, Oxford, 2012, pp. 369–379
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)
Ghezzi, C., Menghi, C., Sharifloo, A.M., Spoletini, P.: On requirements verification of evolving models. In: Submitted for publication (2013)
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
Harel, D.: Statecharts: a visual formalism for complex systems. Science Comput. Program. 8(3), 231–274 (1987)
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)
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)
Object Management Group. The UML profile for MARTE: modeling and analysis of real-time and embedded systems. Online at: http://www.omgmarte.org/
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)
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)
Kwiatkowska, M., Norman, G., Parker, D.: Prism: probabilistic model checking for performance and reliability analysis. ACM Perform. Eval. Rev. 36(4), 40–45 (2009)
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)
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
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
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
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
Van Lamsweerde, A.: Requirements Engineering: From System Goals to UML Models to Software Specifications. Wiley, Chichester (2009)
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)
Young, M., Pezze, M.: Software Testing and Analysis: Process, Principles, and Techniques. Wiley, Hoboken (2008)
Acknowledgements
This research has been partially funded by the European Commission, Programme IDEAS-ERC, Project 227977-SMScom.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ghezzi, C., Sharifloo, A.M., Menghi, C. (2013). Towards Agile Verification. In: Münch, J., Schmid, K. (eds) Perspectives on the Future of Software Engineering. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37395-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-37395-4_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37394-7
Online ISBN: 978-3-642-37395-4
eBook Packages: Computer ScienceComputer Science (R0)