Verifying integration of heterogeneous factory components
Jean-Pierre TALPIN, head of TEA research team
In an automated factory, each equipment or machinery must meet a myriad of constraints. Ensuring that an entire factory chain satisfies these constraints and safety and security regulations requires simulation, test and verification. However, what can be proved when two heterogeneous components, e.g. mechanics and software, interact with each other? How can one prove that this hybrid aggregate also meets common, global, requirements such as, e.g. latency? Such is the question at the crux of a collaboration between Inria and Mitsubishi Electric R&D Centre Europe, two entities located on the same campus, in Rennes, Brittany, France.
A world leader in factory automation, Mitsubishi Electric develops processing machines, servomotors, computerized numerical controllers, industrial robots: equipment to build up a plant from top to bottom. The design of such plants is computer-assisted. All equipment are virtually assembled by the graphical user interface of a software that can produce the floor plans, schematics, specifications and documentation of the plant.
One problem remains, though. “This tool can't verify that the plant will actually work properly and meet the requirements, ” says Jean-Pierre Talpin , head of TEA, an Inria project-team meant to define a framework for reasoning on composition in cyber-physical system design. A concrete example? “Consider the time to halt an industrial robot. For obvious safety reasons, a robot is usually installed in a cage or confined environment. If the door is inadvertently opened, a safety requirement is to stop the robot immediately. The necessary time for the physical system to come to a halt from the moment the “door-opened” event has been registered is called the end-to-end latency. It requires one to reason on both software and hardware of the real-time system and the physic or mechanics of its environment. ”
The question at stake is “how to verify that two components are compatible from the logic viewpoint, the real time viewpoint and the physics viewpoint. ” Such topic is precisely the theme of a PhD thesis funded by Mitsubishi Electric R&D Centre Europe through a Cifre Agreement. Initiated by the French Research Ministry, this grant program helps companies to recruit PhD students who carry out research in collaboration with an academic laboratory.
Compositional Proof in Differential Dynamic Logic
Performed by PhD student Simon Lunel , the ongoing study relies on a formalism of mathematical logic called differential dynamic logic (DL). “This is what best answers the problem, Talpin explains. DL enables to specify and verify a dynamic system with the help of the theorem prover which implements it. This theorem prover allows one to methodically prove that the specification of a continuous system verifies a differential invariant, in other words, a logical property, i.e. a requirement that one wishes to validate. ”
For this work, the scientists have picked ―and enriched― KeYmaera, an open source theorem prover developed at Carnegie Mellon University. “We have contributed to this tool with associative and commutative composition operators and a method to automate the proof of composed invariants (proof compositionality). If I prove invariant “x” for component A and invariant “y” for component B, then when I compose A and B, there is an automated method to prove that AB satisfies property “x and y”. This is called proof compositionality. ”
Beyond the current collaboration, Inria and Mitsubishi Electric are now mulling over a wider partnership. “We are contemplating a framework agreement. In this context, a delegation of the company recently met with several of our research teams from Rennes and Nantes: TEA, Sumo, Celtique, Tamis and Gallinette. Our counterparts at Misubishi R&D happen to be very research-oriented, which makes the dialogue all the more straightforward.”