Position Paper: Formal Methods in Agile Development

Abstract

Modern software development must be agile. It has to accept that soft- ware systems undergo a lot of changes due to changes in the application context (for example changing conditions on the markets and changes due to the jurisdiction) and base technology (e.g. integration of new frameworks or updates of the platform) in their life cycle. Thus, most of the activities in the development process are redesign steps. Even requirements are not stable. They change in time as the context of the system changes. There is no time for complex correctness proofs of the implementation with respect to the requirements. Automatic (regression) testing has proved to be sufficient for correct system behaviour. Therefore the agile developer does not learn and apply formal methods himself. In order to be agile, however, he relies on tools for automatic refactoring of the system or of certain parts of it. These tools are able to change the system structure without changing its behaviour. We argue in this paper that, in order to build such tools, further research in the area of formal system modelling and development is needed.