Using Formal Models as part of software specification in the software lifecycle for the development of high-integrity systems is known to be beneficial in terms of early identification of requirements inconsistencies, providing an unambiguous description of the system before the software is constructed and allowing properties of the specification to be formally proven. However, use of formal models is also viewed by some as a niche skill that requires significant investment, as well as being at-odds with contracts that require early software drops. Viewed as at-odds with typical contract structure because writing the model takes time ahead of coding so may delay the start of implementation. Viewed as niche because many Formal Notations are harder to grasp than the more visual based notations common to Model Based Systems Engineering (for example UML or SyML); on top of which any use of the proof facilities associated with Formal Methods introduces a further barrier to entry. Viewed as expensive because writing a Formal Specification will typically take longer than an informal model. The benefits are only realized through the time saved at integration because there are fewer faults to find – but this is a benefit that can be hard to quantify. There also remain pitfalls with using Formal Models, such as precisely specifying and implementing not quite the system that was required.

Through the SECT-AIR and HICLASS research projects we have been investigating routes to making the use of Formal Methods more efficient. Using the Alloy Modelling language and its associated model checker, the Alloy Analyser, as the foundation of our work we developed algorithms for developing Verification Conditions that achieve specification coverage. The state-of-the-art solvers within the Alloy Analyser can be used to generate test data that satisfies each of these conditions. In principle, this allows implementations in any programming language to be tested against the model using adapters to convert test vectors from the Alloy. When adopting any research initiative in the industrial context there is always a challenge of scalability. Will the technology scale to industrial size problems? Is the approach accessible enough to roll out to a large team of engineers?

I will discuss the experiences of rolling out the technologies described above on an industrial scale project. A project being developed to EN 61508 and using SPARK Ada as the implementation language. I will discuss how it has been necessary to evolve our approach. The problems we found and how we solved them to produce a 20,000 line Alloy specification against which our software developers are able to undertake software component testing automatically and leverage other efficiencies in their development.