Practical experiences of using formal requirements and their role in an overall work-flow

This paper considers the potential benefits and practical challenges of a process using the formalisation of requirements for high integrity embedded software systems. We describe first the translation of software requirements to a formalised notation: Once formalised, the requirements are used as the basis for several high-assurance verification activities including analysis and testing. We describe the approach, motivation and benefits of this workflow, as well as the practical challenges faced and lessons learnt.