Goals of the measurements workpackage Formal methods have been applied quite successfully in a number of industrial case studies and are even adopted in specific industrial fields. However they are still not widely used in the commercial software development, even in safety/security/business critical sectors such automotive, aerospace, e-business. Over time, reasons for this have been widely studied, and a number of obstacles and often misconceptions (“myths”) have been identified such as the difficulty of the maths, the incompatibility to use them with customers, the effect on the costs and delay, the total incompatibility with traditional development methods, the lack of support and tools, etc [Hall90, Bow95]. Guidelines (stated as “commandments”) have also been suggested to address those [Bow95, Bow06]. For adoption, especially by the management level, there is a necessity to provide numeric evidence that formal methods are working. Formal methods can effectively result in improved safety and reliability, but organizations do not always assign direct value to improvements in those areas. In the absence of measurements, formal methods are perceived as a cost [St03]. Management also needs new progress indicators as the introduction of formal methods requires more effort in the early development stages while typically reducing costs at the coding and testing phases. In the absence of such indicators, the management will interpret a project as not progressing. This calls for the deployment of appropriate measurement strategy as companion to the deployment of formal methods. The goal of this deliverable is to propose such a methodology and to validate it on the industrial sectors of the DEPLOY projects. The outcome is not only the methodology, but also the data collected during the project. Its exploitation can provide evidence to educate manager to the adoption of formal engineering methods on real industrial cases and to provide them with guidelines for an optimal deployment in their domain.
