Mitsubishi Electric R&D Centre Europe creates reliable innovation with TrustInSoft
April 20, 2021
Mitsubishi Electric R&D Centre Europe faced the challenge of confirming the safety and reliability of more than 300,000 lines of code
Who is Mitsubishi Electric R&D Centre Europe (MERCE)?
A key component of Europe’s leading R&D community, Mitsubishi Electric R&D Centre Europe (MERCE) researches and develops innovative solutions relating to energy, environment, and communications technologies, including air conditioning and power electronics systems, as well as wireless, optical, and network technologies. The reliability, efficiency, and quality of the company’s products are of the highest importance to MERCE. From information communication technologies to power modules, MERCE uses the best-in-class laboratory equipment and reliable software methodologies to ensure safe, high-quality technologies.
MERCE: Creating 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.
Affirming the safety of safety-critical embedded software
The safety-critical embedded software used in the technology reviewed by MERCE requires a robust code verification to avoid these kinds of challenges that accompany software development and which could lead to safety concerns in the technology and final product.
Researchers at MERCE needed to be sure that no matter what the inputs received by sensors, the software would continue to behave in a deterministic, expected way.
Provided with TrustInSoft Analyzer, MERCE was able to take software verification to the next level. MERCE conducted a comprehensive code review by running source code through the analyzer, allowing for:
- A support of the full C language with all its complexities (pointers, function pointers, explicit and implicit casting, direct access to raw memory and raw memory manipulation, loading of complex data structures in memory, …)
- The detection of even the most subtle undefined behaviors, thanks to the analyzer’s mathematical, formal methods-based approach
- A complement of existing tests, by using symbolic values for inputs. This helped MERCE mathematically simulate in development any unexpected input that the sensors communicating with the software could possibly provide.
- An interactive Graphical User Interface that allows the reviewers to navigate through the source code to locate the root cause of any error. This allowed MERCE to provide clear information to developers on any issues detected by TrustInSoft Analyzer.
Thanks to these powerful benefits of using the formal methods approach, the development team also benefits from more confidence overall that the code they review does not contain any errors that could jeopardize the safety-critical product.
"Tackling the size and the complexity of C code we had to review was not an easy task. It was even quite ambitious when we started this project. TrustInSoft provided to us not only the right tool powered by Formal Methods, which gave us the correctness guarantee level we needed, but also an outstanding hyper-reactive support that allowed MERCE to Get the Job Done."
- David Mentré, Research Manager, Mitsubishi Electric R&D Centre Europe
Key Benefits of TrustInSoft Analyzer in this project
- Application of formal methods to provide mathematical guarantees
- Increased guarantees of correctness for critical software
- Static Analysis Framework with collaborating formal methods
- Compliance with industry standards like ISO 26262, CENELEC EN 50128, DO 178C, IEC 61508, …
- Support for different architectures
- Personalized & dedicated support
- Efficient support from people involved early on in the development of the analyzer
Key Figures
- 7 years of license on 3 projects
- Client since 2014
- 300,000 lines of code in the last project, 120,000 and 80,000 lines of code in previous projects
- Unlimited support & assistance
- Unlimited lines of code
- About 150 tickets opened to TrustInSoft support over the years
Bottom Line
MERCE secures safety-critical embedded software with TrustInSoft Analyzer, to be absolutely sure of their robustness, and to promote their reliability and safety, whatever the environment. Ensuring that the software behaves in a prescribed way, no matter the inputs it receives from the real world, is of the highest importance.
Interested to find out how TrustInSoft Analyzer can help your team? Contact us to schedule a demo!