The French Institute for Radiological Protection and Nuclear Safety (IRSN) set up by law 2001-398 of 9 May 2001, under the statute of public authority of industrial and commercial nature (EPIC) is the national public expert in nuclear and radiological risks.
IRSN contributes to public policy-making concerning nuclear safety and health and environmental protection against ionizing radiation.
As a research and expert appraisal organization, IRSN works together with all the participants concerned by these policies while keeping an open mind.
French nuclear reactors rely heavily on software to perform critical safety tasks.
Because of this, IRSN encourages the use of formal methods to prove the correctness of the software.
This is crucial to ensure the proper performance of the required safety tasks.
IRSN also actively participates in the improvement of tools and their associated analyses methodologies through activities carried out by both research labs and TrustInSoft.
To explore new approaches that prove different structural properties on critical safety C software, IRSN required an advanced and robust static analysis tool with a high level of reactive support.
IRSN became an early adopter of the TrustInSoft Analyzer. They use a license on a dedicated computer to perform comprehensive formal verifications on its C software.
Client since 2014
Analysis of 16 application software programs
18 000 to 24 000 lines of code
230 to 270 functions
340 lines of additional C code written for a single analysis
10 minutes to one hour
Between 0 and a few dozen alarms raised depending on the software analyzed
“TrustInSoft provides a highly advanced static analyzer along with a friendly GUI. Its efficient technical
support is a key point in the success of our software analyses. TrustInSoft helps us understand the
meaning of alarms raised, and provides customized solutions. These efforts are necessary to
understand the possibilities of the analyzer and the scope of the proven properties.”