FBK collaborated with the Emilia-based company, which specializes in industrial automation solutions, by providing advanced automatic verification tools on robot management programs to identify potential risks or inefficiencies.
The Solution:
As part of the European AI-MATTERS project, FBK’s Digital Industry Center (DI Center) collaborated with Robotizr – an Italian company specializing in industrial automation solutions – on enhancing the reliability and safety of robotic systems through the application of formal software verification methods, offering the service: “Application of formal methods for reliable industrial systems.” The Robotizr platform allows industrial robotic arms to be programmed via an intuitive graphical interface that enables the creation of operational sequences through the composition of visual blocks on tablets, even for operators who lack programming skills. This flexibility opens robotics to new users and contexts, but it also introduces the need to ensure that the programs generated are safe, consistent, and efficient.
The Formal Methods Unit of FBK’s Digital Industry Center, thanks to the AI- MATTERS service, has integrated advanced automatic code verification tools developed in-house by the Foundation(model checker nuXmv, Kratos analyzer) for the purpose of analyzing user-generated programs and automatically detecting anomalous behavior, inefficiencies or potential risks before the robot goes into operation.
The result was the validation of a platform that combines accessibility and security, capable of preventing operational errors and ensuring greater reliability of production processes.
The delivery of this service highlighted how applied research can be the basis for validating concrete solutions developed for industry, promoting intelligent, safe and sustainable automation in line with the principles of reliable Artificial Intelligence.
The Solution
AI-MATTERS provided Robotizr with customized technical expertise and access to cutting-edge verification technologies developed by FBK’s Formal Methods (FM) unit.
The project focused on integrating formal verification methods directly into the Robotizr platform, using advanced tools such as the nuXmv symbolic model verifier and the Kratos code analyzer.
Through this collaboration, the Robotizr team, along with FBK researchers Stefano Tonetta and Alberto Griggio, designed a verification backend that can translate the robots’ visual programs into formal representations, automatically checking for anomalies, unreachable blocks or unsafe movements.
The results
The partnership between Robotizr and AI-MATTERS has produced measurable results:
Increased safety: early detection of unsafe or inconsistent robotic behavior.
increased reliability: automated validation of user-defined programs through formal analysis.
improved usability: users can now receive real-time feedback on potential errors directly within the visual programming interface.
These advances have transformed Robotizr’s platform into a reliable industrial automation environment where safety and innovation coexist.
Looking to the future
Validation in demo environments and at the MADE competence center showed exciting results, Based on the results obtained with AI-MATTERS, Robotizr plans to expand its verification framework to include dynamic runtime analysis and machine learning-based optimization, ensuring that automation remains intelligent and secure.