Validation and Verification
The first step to seeing how formal methods for software verification and agile methods of software development can be complementary is to come to terms with the difference between Validation and Verification. Software validation is about asking the question "Are we building the right product?" while software verification is a matter of asking "Are we building the product right?". In general Agile methodology focuses mostly on software validation - getting working prototypes in front of the customer as soon and as often as possible to get as much regular feedback about exactly what is wanted as early in the development process as possible. From the Agile point of view there is no sense designing and building something the customer doesn't want, so early and regular feedback is key; moreover there is no point writing anything more than the minimum required to meet the clients needs at any given stage. In short, you want to be sure you're building the right product - that it has what the client wants, and that you're not wasting time on things the client doesn't care about.
In contrast formal methods focus on software verification - formalising requirements into a specification, and using those specifications to get early and regular feedback as to whether the implementation actually meets the requirements. Formal methods tend to have little or no interest in the validation side of the equation - determining whether the specifications will build the right product is considered a separate concern. Instead the focus is squarely placed on making sure the code you do right does exactly what you claim it does. From the formal methods point of view there is no sense relying on programmers to eventually spot that their code doesn't actually do what the informally written requirements actually demand; document requirements precisely and early and then let the computer do the work in an automated fashion - bugs caught early are much cheaper to fix than bugs eventually spotted down the road.
There is, of course, a certain amount of overlap. Formal methods tend to do a certain amount of software validation by working with the customer to refine a detailed formal specification. Agile methods attempt to handle software verification by means of unit tests. In practice, except for particular projects well suited to each approach, this overlap portion represents the weakest aspects of both methodologies: hypothetical models based on formal specification are a lot harder for clients to deal with than working prototypes and mock-ups; Unit tests offer, at best, rough case-wise specifications and leave plenty of scope for unforseen corner cases, and unexpected behaviour.
Agile Formal Methods
The obvious approach, then, is to try and take the best aspects of each approach and use them to bolster the weak points. This is actually surprisingly easy. Simply take an Agile approach, such as Test Driven Development, and augment the weaker Agile "verification via unit testing" with lightweight formal specification and the far more powerful verification that then becomes possible. You retain the Agile approach with rapid and regular customer feedback, including such things as Fit acceptance testing, while getting the strength of formal methods for verification: instead of just adding new unit tests, you add or refine the specification.
Isn't writing formal specifications all the time too hard, and formal verification just too much hard work? Perhaps, but there's a reason I said lightweight formal specification - a great deal of formal specification can be achieved easily using contracts which, when using JML for Java, Spec# with C#, or Eiffel, are no harder to write than the equivalent unit test. In practice writing a contract is actually simpler, and requires less framework and template code, than writing the equivalent unit test. As for how hard the resulting verification process is - it turns out to be very efficient: JML for Java supports ESC/Java2 for very practical yet powerful verification, while Spec# includes its own similar verifier, and there are many other tools available which will be discussed later. Modern verifiers such as ESC/Java2 and the Spec# verifier take a pragmatic approach, making use of the specification to do a raft of static checks, proving what they can, and simply warning about what they cannot - they integrate easily into modern IDEs like Eclipse and VisualStudio, and generally take around the same length of time to run as a compiler or unit test suite.
Is this approach really practical? Yes, it is - there is already a system for Eiffel called ESpec that provides an integrated workbench for exactly this design approach, seamlessly integrating Fit testing and Agile software validation techniques with formal specification, and code verifiers. Even if Eiffel isn't your language of choice it may still be worth a glance since similar systems will more than likely soon start appearing for Java and C#.
What Does it Do for Me?
Given the ingrained resistance to formal methods in the Agile community due to historical arguments and a lot of mistaken assumptions from both sides, it is worth outlining what adding lightweight formal methods to the traditional Agile process can actually do for you. The first win, and this may sound odd, is that it is actually less work! Given a good contract system such as that of Eiffel, JML, or Spec#, writing formal specifications is often easier and involves less redundant template code than writing the equivalent unit test. Of course not everything can be efficiently expressed as a contract - but no one is asking you to do away with unit testing, ESpec, for instance, specifically integrates unit testing into the workbench to cover cases that are more easily specified as tests rather than contracts. What a little specification really buys you, however, is far more powerful verification and testing - so lets talk about some of the sorts of tools that are available.
The power of extended static checking should not be overlooked. You can think of it as lint on steroids if you like - but it is definitely worth taking a look at what modern extended static checking using contracts can do. Essentially the static checkers analyse the code and contracts checking both for common errors (much as lint does) as well as attempting to verify that the code meets the contracts using theorem provers. Counterexamples will even be generated in cases where contracts will not necessarily be met. ESC/Java2 can catch everything from potential null pointer exceptions to possible race conditions. And all of this can be seamlessly integrated into your existing IDE. Extended static checking catches potential bugs early, and catches bugs that will be missed by all but the most exhaustive of testing.
The other push button power tool is automated testing. Again it is Eiffel that offers the most robust solution here with AutoTest, but similar tools are in development for Java, and for Spec#. The idea is simple enough - use contracts as a test oracle and generate random test data. In the case of AutoTest this has produced a tool in which the developer simply presses a button and walks away and the code is exercised automatically, over a vast array of possible test cases, and a simple final report with simplified failure cases is presented at the end. Test data can be generated by many different schemes, from purely random, to genetic algorithms, to schemes designed to provide maximal search space coverage. Failing test cases are even automatically added to unit tests for regression testing. This sort of thrash testing really is effective: AutoTest successfully uncovered bugs in the Eiffel base libraries that had gone unnoticed for over a decade.
By combining these approaches we arrive at a level of robustness checking and software verification that basic unit testing simply cannot match - and all at no significant extra cost. By writing contracts instead of unit tests wherever it makes sense we enable far more powerful static checking and provide the necessary extra information for completely automated thrash testing.
As much as it may surprise those who are used to the ideological divide, Agile Formal Methods really can work - complementing each other very naturally to provide a far better system than either methodology can offer alone. Moreover this sort of pragmatic lightweight formal method approach is beginning to seriously gain traction with JML and Spec# becoming increasingly popular. Already Agile Formal Methods suites are available for Eiffel, and we can expect that it is only a matter of time before similar systems become popular for Java and C#.