Rod Chapman and his co-authors Neil White and Jim Woodcock mention how the use of SPARK fits in the agile approch to high-integrity development at Altran in this article published in the October issue of the renowned magazine Communications of the ACM. We've mentioned the work of Rod (at Altran and other places) many times on this blog, see his presentation at Bristech earlier this year for his take on the place of formal verification for security.
Here is a brief excerpt:
The NATS iFACTS system augments the software tools available to air-traffic controllers in the U.K. It supplies electronic flight-strip management, trajectory prediction, and medium-term conflict detection for the U.K.’s en-route airspace, giving controllers substantially improved ability to plan ahead and predict potential loss-of- separation in a sector. The developers precede commit, build, and testing activities with static analysis using the SPARK toolset. Overnight, the integration server rebuilds an entire proof of the software, populating a persistent cache, accessible to all developers the next morning. Working on an isolated change, the developers can reproduce the proof of the entire system in about 15 minutes on their desktop machines, or in a matter of seconds for a change to a single module. While Agile projects might have a “don’t break the tests” mantra, on iFACTS it’s “don’t break the proof (or the tests) ... ”
Well done Rod.