Mitsubishi Electric R&D Centre Europe creates reliable innovation with TrustInSoft

MERCE faced the challenge of confirming the safety and reliability of more than 300,000 lines of code to make up a new, safety-critical embedded software which is intrinsically very complex.

The embedded software is used in a variety of configurations, which means it needs to function on a variety of different materials, each with their own constraints. The equipment’s sensors could receive a large variety of different signals, generating different inputs for the software’s code functions. Testing the software in production is complex and time-consuming, and it is impossible to manually test for every possible input. 

Safety-critical software must take into account all possible values for these inputs.  But to be sure that the software responds in a predetermined way no matter the input requires developers to use tools that are more extensive than traditional tests.  With mathematical tools, this becomes possible. MERCE’s mission is to find such advanced, mathematically based tools and to design adequate methodology for their effective usage.

This is the reason why MERCE chose TrustInSoft to provide their research team with the tools they needed to do such kind of source code analysis.  TrustInSoft Analyzer provided the mathematical solution to prove the correctness of the software development process, from code development perspective, using formal methods.

Ensuring the safety and reliability of complex technological systems requires surmounting certain challenges to secure software development:

• The ability to expect the unexpected – even if a test existed for every line of code in a program, using discrete values for test inputs is inherently limiting, and thus limits the effectiveness of the tests. For the embedded software reviewed at MERCE, expecting the unexpected is a necessary part of secure code development, to avoid undefined behaviors resulting from unanticipated inputs, like exceptional values sent by sensors.

• Detection of the most subtle undefined behaviors – even a comprehensive approach to code safety with traditional testing tools cannot systematically identify every undefined behavior. This can be crucial for a safety-critical application, where just one error in the code can lead to dangerous consequences.

• Increase in code complexity – as years go by, the number of lines of code necessarily increases, including to patch bugs, and the software developers maintaining it may change over time. This means that as the world becomes more and more dependent on software, the more and more the software will become more complex.  This intensifies the need for secure software and the difficulty in finding errors in the source code.