Formal methods and continuous change: towards a happy marriage

Formal methods have now matured to a stage where models of real systems and complex programs can be verified against realistic requirements specifications through efficient procedures. Automated dependability assurances for real-life systems have become possible. Why mainstream software development processes still largely ignore formal methods? Why, for example, has test-driven development shaped iterative, change-oriented, agile processes while formal modelling and verification are largely dismissed? Whys is software evolution and change still practiced with little or no use of formal methods? I will argue that a not-to-be-missed opportunity exists today for software engineering research to remedy this unfortunate divergence between modern development processes and formal methods. More generally, I will argue that formal methods and continuous change can be reconciled and combined through a happy marriage. I will discuss why this is important and I will argue about what should be done to make this happen. I will get to this point by looking backwards at a number of past research efforts, including some personal experience reports, trying to identify what lead to the current stage, making the happy marriage now possible.