Evidence on Formal Methods uses and impact on Industry
Motivation & Objectives
Many organizations wonder how formal methods could be used in their sector, on what type of applications and product and at what stages of the development lifecycle. However, they currently find a lack of information on what they could face when taking up formal methods. Woodcock et al.'s survey of 62 industrial use cases further highlighted this issue (full survey paper & short summary). The important concerns related to formal methods expressed in this survey are:
- Collect pieces of evidence of Industry uses of formal method (first time and subsequent uses)
- Improve tool support
- Break the psychological barriers on skills required to master formal methods
The main objective of this wiki is to present information related to the use and the impact of formal engineering methods in Industry. It is not intended to be a tutorial on any given method but rather it assemble information extracted from Industry use cases. Based on this, organisation considering the adoption of formal methods have a comprehensive view on the impact of the use of such methods at the different stage of the product development cycle.
This site directly targets the first concern by presenting pieces of evidence from industrial uses of formal methods. It also indireclty addresses the other two issues presenting several pieces of evidence related to tools quality, maturity of tool support and training of people with and without background in formal methods. A specific page is also dedicated to the presentation of Useful wiki features that can guide you in finding your way in this repository.
Audience and Usage Scenarios
Deploying any new development methods has multiple impacts at differents organisation level. In order to best reflect those, it is useful to take an approach combining multiple viewpoints, corresponding to important roles in an organisation that will be part of the change and will have to consider specific issues (such as scope, training, roll-out, tools...) in order to take a decision. Four Roles have been defined for this (High-Level Managers, Project and QA Managers, Engineers and Analysts, QA Practitioners).
In order to help in the use of this evidence repository, a number ot typical Usage Scenarios have also been defined.
Two complementary methods are used to present pieces of evidence on important topics related to formal method take-up in Industry:
It lists frequently asked questions on important themes related formal method adoption. Each Question is role-based, that is, it is asked and answered from the viewpoint of a particular role in an organisation ranging from higher level management, project management to analysts and engineer. Rather than segmenting answers on sector, the goal of the FAQ is to harmonize cross-sector answers to encourage various sectors to share their experience on the different formal method topics covered in this FAQ.
The DEPLOY project is one of the largest, if not the largest, research project on formal methods ever undertaken. DEPLOY involves many research and industry organisations working hand-in-hand to accelerate the take-up of formal methods. This active collaboration gave birth to a set of success stories. Unlike the FAQ, success story are organisation specific hence a sector specific classification seems more adequate.
Why two presentation methods: FAQ and Success Stories
- A success story presents a continuous piece of text that is likely more pleasant to read when in an exploratory search to discover how others have been successful in their adoption of formal methods.
- FAQ is likely more useful to understand specific challenges that will need to be solved if one attempts to integrate formal methods in an organisation.
Some FAQ about our FAQ
Q: How to contribute to the FAQ or to Success Stories ? A: Contributions are very welcom and can range from quick questions/comments to more elaborated contributions in a specific FAQ or even a full success story. Our Procedure page describes in more details how one can contribute information. If you have actively been using formal methods, we also invite you to fill the ACM Survey
Q: Who manages the content and evolution of this work ? A: To guarantee the integrity of the information found in this wiki, an Editorial Board has been created. Information related to this board as well as how to become an active member is described in the related page.
Q: What is the general roadmap, especially after the end of the DEPLOY project ? A: This evidence repository will not end with the DEPLOY project and will continue to be maintained and to evolve after the end od the project, see our Roadmap page for what to expect.