Above: Hinkley Point C construction site, as of early May 2020 (photo: EDF)
Atkins will use MALPAS software, for which it has exclusive rights of use. The verification will include a trial analysis to fully demonstrate the use of MALPAS and fully define the methods to be used. This will be the biggest formal proof yet completed using MALPAS, though it will not be the first time it has been used to assess reactor protection software, having already been employed for the Temelín nuclear plant in the Czech Republic and Sizewell B in the UK.
John Drever, advanced engineering and technology practice manager at Atkins, said: “As the world becomes increasingly digitally enabled, and software embedded into safety critical operations, tools like MALPAS will be integral to ensuring the safety of our systems and critical national infrastructure. This appointment is at the heart of Hinkley Point C’s programme.”
The MALPAS toolset consists of a number of analysers which focus on different aspects of software correctness and integrity. These analysers work with a MALPAS Intermediate Language (IL) representation of the software program which is being analysed.
IL is a universal sequential programming language into which programs written in other languages are translated (via automatic or manual means). The benefit of this process is that the MALPAS analysers need only know about IL, but the analysis results are relevant to the original program, meaning that the MALPAS analysers are essentially universal.
