Mitsubishi Electric R&D Centre Europe

Creating Reliable Innovation with TrustInSoft

Context

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. 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. 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. TrustInSoft Analyzer provided the mathematical solution to prove the correctness of the software development process, from code development perspective, using formal methods.

Implementation

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.

Results

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
The detection of even the most subtle undefined behaviors,
A complement of existing tests, by using symbolic values for inputs.
An interactive Graphical User Interface

Key figures

0 years of license on 3 projects

0 lines of code in the latest project. Previous projects: 80,000 and 120,000 lines of code

Unlimited

support and assistance

“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 use 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, MERCE