By using parameterisation and generalisation of specification/modelling/verification problems, as well as by using modular representation.

If you think about agile development as about "building something out of LEGO", where customer can combine LEGO pieces together a he wish and also add his own pieces, then you could "verify the pieces" that are especially critical.

Formal verification is expensive nowadays, it makes sense to verify only the parts of system that are really safety-critical. Thus, you get a verified core of you system (e.g., for a vehicle: airbag functionality, ECall, etc.) and only tested entertainment part.

I second Maria Spichkova: modularity and generalization/refinement is key. I also second Nick Battle that papers from the first and second workshop Agile Methods & Formal Methods (AMFM) are suitable (I also have one on my researchgate-page about refinement for checking ioco embedded in Scrum).

In order to made this integration in my experience you have mix both alternatives. The agile development process is open to many changes in the software during the development process because the client is part of the development team so the mathematical verification methods for a better quality can be consider a tool before release any critical part of your software. However do not let down the agile development verification process. In order to release a highly good software you have to made as much test as you consider.

Hi,

In my opinion, since the reason of discovering agile methodologies was to avoid formal processes which require tedious works (however, these tedious processes are essential for critical systems), there is no way to integrate those unfortunately. Agile methodologies are more appropriate to be used in compact and short/medium term non-critical projects, not in critical projects that highly require formal methods to verify them. Perhaps, in near future lighter or reduced version of formal methods (is semi-formality possible?) which can be applied with agile methods, will be developed, the integration would then be meaningful and possible.

It's a matter of value. In Scrum, the PO has to be convinced that formal modelling (or other formal techniques) have value above cost. If so convinced, the PO can make the corresponding engineering practices part of the Definition of Done. The Product Owner may herself use formal specification techniques if they are made transparent and if it can be shown that the benefit outweighs the cost. Both of these, of course, depend on doing true Scrum where the PO really is the boss and really has final say over the product vision, final say over the PBIs on the Product Backlog, and the wherewithal to come together with the team on the corresponding components of the Definition of Done.

To disagree slightly with Nick: Keep in mind that working code is not the first priority — it's self-organisation and feedback in Agile, and it's people and Kaizen mind in Lean and in Scrum. Few formal methods cater well to that agenda.

To disagree slightly with Yasar: Agile says nothing against tedious work.

To disagree with Maria: A system is as weak as its weakest link. Using formal methods on one part to robustify it does not make the system robust; there are many formal proofs around this concept. What she describes takes quite advanced risk analysis techniques; these are the purview of the PO, supported by input from the development team.

The constraints of any given formalism are necessarily arbitrary at some level because they encode assumptions. Let's say that you derive formal requirements to control flight trajectory. In a purely mathematical formalism you can make this arbitrarily precise. It's been done many times. Early missile guidance systems were thusly formalised.

What they found in early rocket systems is that the cancellation errors of the floating point hardware accumulated over each cycle of the trajectory calculation, causing the missiles to miss their targets by several hundred meters.

I have dozens of examples like this. I was at AT&T for 20 years and our experience with formalisation was that it was great for simple problems — well, it was great for those who were pushing formalism. It cost more than empirical and experimental techniques.

In theory there is no difference between theory and practice; in practice, there is. So, in practice, you need feedback. Formal specs are usually extremely costly and their use is usually limited to extremely high-risk situations. On the other hand, well-defined feedback loops are very cheap. Formal systems add delay and slow learning; well-designed prototypes give more faithful in-context insights into emergent requirements for complex systems than a formal analysis ever well. Further, replacing formal specs with small empirical increments covers a multitude of other sins, such as bad requirements or assumptions that would otherwise blindly be encoded in a formal spec.

Formalism has its place; after all, a C compiler implements a very complicated but formal transformation from source code to object code. But it is only complicated: I can perfectly reason about its function beforehand and perfectly analyse its results afterwards. In complex phenomena I can do only the latter. In chaotic phenomena I can do neither. Formalism has very limited application in complex phenomena — things that don't obey the laws of physics. Like Facebook. Like your checking account. Like any software. Software is not subject to the laws of physics.

Specification also has its place. In Scrum we insist on enabling specifications for the team. That doesn't mean they are formal. Instead, we communicate them in a process of feedback. The dozens of feedback loops that happen in Sprint Planning are worth a thousand formal specs.

If you look at the Danish space program — which will probably put a human into suborbital flight this year — they de-emphasise formalism and are using experimentation and feedback. It's very much a throw-it-together-and-see-if-it-works culture, directed by someone with deep NASA experience. They're going to achieve their goal this year after having started in 2008 and operating on a budget of about $100,000 per year.

You couldn't afford to do the formal spec alone for that much.

It sounds like your systems are only complicated and not complex. Anything that succumbs to mathematical analysis is a pretty easy problem. Agile deals best with complex problems; it may be overkill for what you describe as your work.

You say your formal approaches are unrelated to proofs. Formal can mean two things. It can mean "having form" or it can mean having the ability to derive (prove) specific properties. I think it's misleading to use the first and is simply for its own sake if it is the second.

For an understanding of the difference between simple, complicated, complex, and chaotic, look into the Cynefin model.