Inria and Mitsubishi Electric collaborate to develop a digital copy of an industrial assembly line

In an automated factory, each link in the manufacturing chain must take a whole host of constraints into account, in addition to meeting a range of requirements. In order to ensure that these are properly respected by the production line, each component has to be simulated, tested and checked. But what can be proved formally when two heterogeneous components interact with each other? e.g. a piece of software and mechanical parts? How can it be proved that these hybrid combinations meet shared requirements, such as a minimum latency delay, for example?

For years now, these questions have stimulated conversations between Jean-Pierre Talpin, head of the TEA research team at the Inria Rennes - Bretagne Atlantique Research Centre and David Mentré, head of the INS team at the Mitsubishi Electric R&D Centre Europe (MERCE). Based on the same campus, it is one of the group’s biggest research units outside of Japan.

“Following discussions, MERCE eventually decided to fund a PhD, which is our standard way of moving forward when collaborating with academic research laboratories”, explains David Mentré. “Simon Lunel was the student selected for this PhD, which was primarily aimed at producing a composition theorem which, when given two components for which we have the respective guarantees, would automatically provide the overall guarantee”. As Jean-Pierre Talpin points out, this PhD on the compositionality of proofs had a surprising impact: “it enabled a contribution to be made to KeYmaera X, an opensource theorem prover developed at Carnegie Mellon University in the USA.”

There have been a number of one-off collaborations between Inria and MERCE in the past.

“Around 2012, we started working with the Toccata team at the Inria Saclay - Ile de France Research Centre”, explains David Mentré. “They are responsible for developing Why3, a proof environment used to prove properties with multiple languages. We also funded a PhD within the πr² team in Paris, which began in 2014.”

All of this led MERCE and Inria to consider a more general agreement aimed at facilitating any point-to-point collaborations which could arise in the future. “This framework agreement will iron out the problems normally encountered when putting this sort of partnership together, beginning with how intellectual property is divided up. Once all of that has been properly codified and the rules established, it will then be much easier for scientists from both our institutions to work together. If we want to fund a new PhD, for example, all we need to do is add an amendment to the main agreement.”

Indeed, funding PhDs is very much the order of the day. “There are a whole host of case studies in the corporate world.” Despite the industrial context, “PhD subjects are often highly theoretical. We give students a great deal of freedom when it comes to deciding on their subject. We don’t demand ready-to-use applications that we will be able to transfer to our commercial divisions in the short-term or anything like that. If we find ourselves in a situation with research that is only in its infancy, then that’s not a problem. In any case, in a group of 140,000, these results may be of interest to many people.”
MERCE is currently funding two PhDs. “Stéphane Kastenbaum began his in October 2019. He is currently studying within the TEA team, following on from where Simon Lunel left off. Simon had proposed a theoretical breakthrough in modular verification. Stéphane will perhaps look for more algorithmic results: how can previous research be incorporated into a programming model similar to the one used by Mitsubishi Electric? Emily Clement, the other PhD student, began her research within the Sumo team back in December 2018, focusing on the ability of clocks to handle imprecision in the verification of timed automatons. This research is also very much in its infancy. We are looking into funding another PhD within the Gallinette team (an Inria team set up to study proof assistants).”

“There are also two other collaborations ongoing with Inria. The researcher Reiya Noguchi left Japan to spend several years with us at the R&D centre in Rennes. He visits the Sumo team at Inria once a week to work on the verification of timed automatons. Scientific production is shared with three researchers from this team: Nicolas Markey, Thierry Jéron and Ocan Sankur.”

“Mitsubishi Electric is also a stakeholder in the ProofInUse.” Launched by Claude Marché, head of Toccata, an Inria team, and funded initially by the French National Research Agency, the purpose of the first version was to inject Why3 into SPARK, a programming language formally based on the programming language Ada, developed by the company AdaCore.

ProofInUse 2.0 is currently being prepared. Mitsubishi Electric and other companies will become partners in this. However, putting together a consortium with multiple members is proving more complex, and it will be a while before this is signed. In the meantime, we have reached an agreement with Toccata to begin an 18-month collaboration. This interim partnership was made possible through the MERCE-Inria framework agreement.

What is the overarching objective of all of this?

“To develop a digital copy of a factory”, explains David Mentré. “Formal methods and the compositionality of proofs for cyber-physical systems, including continuous systems, will help us to develop a digital duplicate of the physical installation. One day, we hope to be able to design and simulate processes, before using that as a basis to build a physical factory capable of running smoothly from day one. This is the Holy Grail for us. There will be a few PhDs between now and then, however...”