Formal Safety Analysis in Modular Robotic Applications
The ForSAMARA project focuses on formal verification of collaborative robotic applications against safety properties. In particular, we apply model checking methods where safety-critical situations can be identified by the result of a mathematical verification proof during the design time.
On the first side, this method is very powerful in its verification significance, but on the other side, model checking still suffers a complexity problem. Thus, behavioral and architectural models of robotic components have to be abstracted to reach a clear balance of verifiability and expressiveness in order to get valuable verification results.
Our motivation and expected industrial impact is a further step towards pushing formal verification methodologies into an industrial model-driven software and system design flow for robotic systems. Especially the feature of reflecting system safety requirements as properties and showing that they are unambiguously fulfilled in the designed system model can be very beneficial in modern I4.0 applications where complexity and application agility is steadily increasing.
Watch the presentation of the ForSAMARA ITP at ERF 2020 in March
