Going Large with Formal Methods on iFACTS

Presented as part of the 2014 HCSS conference.

Abstract:

The iFACTS system provides electronic flight-strip management, trajectory prediction and conflict detection for en-route air-traffic controllers in the UK. The development of iFACTS used “formal meth- ods” in various contexts, including the functional system specification and the implementation, which is subject to various levels of static verification and proof. The formal specification is possibly one of the largest ever produced or reported, and the implementation runs to over 200kloc, with a team size that peaked at over 130. The system is in fully operational service, meaning 24 hours per day on all sectors.

Rather than focusing on the technical aspects of the iFACTS effort, this presentation will concentrate on the perceived usefulness, scalability, training needs, and metrics from the various “formal” aspects of the project, and the lessons that we’ve learned along the way. 

Presenter Bio:

Rod Chapman is a Principal Engineer with Altran, specializing in the design and implementation of safety and security-critical systems. He currently leads the development of the SPARK language and its associated analysis tools.

Rod is a well-known conference speaker and has presented papers, tutorials, and workshops at many international events including STC, NSA HCSS, SIGAda, Ada-Europe and the Society of Automotive Engineers (SAE) World Congress. In addition to SPARK, Rod has been the key contributor to many of Altran's major projects such as SHOLIS, MULTOS CA, Tokeneer and Software verification tools. He received a MEng in Computer Systems and Software Engineering and a DPhil in Computer Science from the University of York, England, in 1991 and 1995 respectively. He is a Chartered Engineer, a Fellow of the British Computer Society, and also an SEI-Certified PSP Instructor.