Accessible formal methods in Nuclear Engineering

The use of formal methods is widely acknowledged to be best possible practice for assuring the behaviour of software systems but is still thought to be inaccessible to a typical software engineer. Furthermore, often the prevailing view is that formal methods are only accessible by academics and that evidence to support certification can be difficult to obtain. Finally, that they are typically applied only after all the development has been undertaken in order to provide extra assurance.

The presentation explores how the state of the art for the use of accessible formal methods could be used throughout the development of control systems in the nuclear sector, rather than being applied after a development is notionally complete.  

A case study was funded by the Control and Instrumentation Nuclear Industry Forum (CINIF) to explore the use of commercially supported formal methods tools.  The tools and techniques are accessible without any formal methods knowledge; typical software engineering skills and domain knowledge are all that are needed. 

The webinar will highlight how an informal specification (‘customer requirements’) was used as the basis for the development of a set of system requirements using structured English and shows how exploration of desired properties at the requirements level can be explored formally. The case study continues by showing how formalism was introduced through software requirements, design and code and used as the basis for automatic, independent verification and the potential for formal verification of the Executable Object Code is also discussed. The possible claims for certification credit are presented based upon the use of RTCA DO-333, the Formal Methods Supplement to RTCA-DO-178C, the only published ‘standard’ for formal methods; a summary of the claims is provided, including limitations.

Finally, metrics are presented, including the hours of effort expended on development and verification.