Formal Versus Agile: Survival of the Fittest?
The potential for combining agile and formal methods holds promise. Although it might not always be an easy partnership, it will succeed if it can foster a fruitful interchange of expertise between the two communities. In this talk I explain how formal methods can complement agile practices and vice versa. There are no pre-requisites for this talk, except an open mind and a desire to make software development more reliable. Leave any pre-conceptions at home, and be prepared for myths to be dispelled.
Paul Boca is currently Quality Engineering Manager at Hornbill Systems Ltd, working on software quality initiatives and process improvement. Prior to joining Hornbill, he was R&D manager at static analysis vendor PRQA. His early career was spent in EDA, specifically hardware compilation, working for Sharp's European research Laboratory and then Celoxica. He organises evening seminars to promote formal methods to a wider audience and has recently edited a book of papers based on these seminars.
His current interests are in software quality, program transformation and analysis, formal methods, software engineering. He graduated from Queen Mary, University of London, with a PhD in Computer Science, exploring categorical properties of program transformations.
Formal Methods: A Extensive Survey of Practice and Experience
Formal methods use mathematical models for analysis and verification at any part of the program life-cycle. We describe the state of the art in the industrial use of formal methods, concentrating on their increasing use at the earlier stages of specification and design. We do this by reporting on a new survey of industrial use, comparing the situation in 2009 with the most significant surveys carried out over the last 20 years. We describe some of the highlights of our survey by presenting a series of industrial projects, and we draw some observations from these surveys and records of experience.
Based on this, we discuss the issues surrounding the industrial adoption of formal methods. Finally, we look to the future and describe the development of a Verified Software Repository, part of the worldwide Verified Software Initiative. We introduce the initial projects being used to populate the repository, and describe the challenges they address.
Jim Woodcock is Professor of Software Engineering at the University of York, known for research, teaching, and consultancy on industrial-scale formal methods, including IBM CICS, DEC Spiralog, Mondex, railway signalling, and the nuclear industry. He is editor-in-chief of Formal Aspects of Computing Journal and a visiting professor at universities in Europe, Asia, and the Americas. His current research projects include: the high-integrity Java HiJaC project; the interdisciplinary InDeED project; an NPL partnership on verifying scientific software; verifying the integrated European railway signalling system (InESS); a UK-India project on verifying embedded systems; and an industry project on verifying secondary protection systems for nuclear reactors. He leads the UKCRC Grand Challenge on Dependable Systems Evolution and its international cousin, the Verified Software Initiative (VSI), and coordinates its international contributions, particularly experimental work for the VSI's repository. His key contribution has been to collect and promote a series of problems for pilot projects. This work has had a considerable impact: he has assembled an international team of 55 different institutions world-wide. They have already contributed work to at least one of the following pilot projects: the Apache web-server, the Cardiac pacemaker, the POSIX-compliant flash-memory space-flight file store, the FreeRTOS real-time operating system, various hypervisors, the Mondex smartcard, and the Tokeneer ID Station.
Open-DO Update: A review of the latest news and developments with the Open-DO effort.
Cyrille Comar is co-founder and Managing Director of AdaCore Europe. He is one of the key architects of the GNAT compilation technology, and he led the implementation of the Ada 95 object-oriented features and the GNAT library model. With a deep interest in safe and secure programming and certification, Cyrille is actively participating in the DO-178C Working Group and its Object Oriented Technology subgroup. Cyrille has published numerous papers on GNAT technology, software quality and multi-language programming. He holds Masters and PhD degrees in Computer Science from Universite Marie et Pierre Curie (Paris 6).
Formal Method for Avionics Software Verification
From real use for Airbus aircrafts to the integration in ED-12C/DO-178C
This talk will give examples of Airbus use of Formal Methods to verify avionics software, and summarises the integration of Formal Methods in the upcoming ED-12/DO-178 issue C.
Firstly, examples of verification based on theorem proving or abstract interpretation will show how Airbus has already taken advantage of the use of Formal Methods to verify avionics software. Secondly, we will show how Formal Method for verification has been introduced in the upcoming issue C of ED-12/DO-178.
Hervé Delseny works as an expert in Avionics Software Aspects of Certification at Airbus. He holds a master’s degree in industrial software from Tours University in France. Since 1992, Hervé heads a team in charge of methods and quality for software developed by Avionics and Simulation Products. Avionics and Simulation Products is the software & electronic centre of expertise and the internal avionics supplier of Airbus, which develops software for flight control, flight warning and communication equipment for all Airbus A/C families. Prior to that, Hervé developed the secondary flight control software for A340. He is currently involved in the joint Eurocae and RTCA working group in charge of writing issue C of ED-12/DO-178. In this working group, Hervé has mainly focused his efforts to improve ED-12/DO-178 to take into account Formal Method and to promote the use of Formal Method for avionics software verification.
The Use of Formal Methods on the iFACTS Air Traffic Control project
This talk provides an overview of the formal methods used on the iFACTS project. iFACTS is delivering increased Air Traffic Control capability to the UK. This is achieved through the elimination of paper flight strips, and consequently improved aircraft conflict detection and the provision of "what if" functionality. The project uses a mix of formal methods including a specification in Z, an implementation in SPARK Ada, and algorithm modelling in Mathematica. The talk will cover the challenges and successes of deploying formal methods industrially on a project of over 120 engineers in three countries.
Neil White is a Principal Engineer with Altran Praxis. Neil has been involved with the delivery of safety-related and safety-critical systems for many years. His experience covers the aerospace, defence, naval, and finance sectors. Currently he is the Engineering Manager for the iFACTS programme. Neil also leads the Software Practice within Altran Praxis, setting strategy and providing guidance for the company's software direction.
Agile Methods and Safety-Critical Software
This talk surveys Agile methods and formulates a list of features that occur in these methods, then considers whether each of the features can be applied in the field of safety-critical software development. The talk concludes that almost all of the features of Agile methods are applicable to safety-critical software but that existing standards are a problem for Agile’s de-emphasis of design and documentation. The talk will also look for quantitative evidence in the published literature for the benefits of Agile methods in software development in general, and surveys various published opinions on Agile’s application to safety-critical software development.
Dr Peter Gardner has twenty years experience in languages and software development methodologies and acts as the focal point for UML in Silver Atena. He is interested in issues such as continuity between function-based and object-based modelling, and the contrast between the Agile approach and model-based development. He also has a background in numerical algorithms and his doctorate is in solid state physics.