Parametric formal verification: the robotic paint spraying case study

The design of robots in industrial automation is based on classical control theory approaches. Recently, formal verification methodologies have been introduced in the design flow, due to their ability of analyzing the model of the robot-environment system in a conservative way. In this paper we specifically explore the analysis of system parameters within a continuous space, by developing an extension of the tool Ariadne for reachability analysis of hybrid automata. Under this framework, the system takes the form of a composition of automata which model discrete control parts that operate in a continuous environment. In particular, the dynamics of the system includes parameters, i.e., unspecified constants for which we want to observe the effect on the dynamics, with the purpose of finding optimal design values. As a case study for this methodology, we consider a robotic paint sprayer, in which we use Ariadne to study the effect of choosing different values of a parameter that represents a point of observation for the system. Using the information gathered from this automated analysis, we provide an answer to the problem of optimizing the surface spraying speed while respecting a given measure of spraying quality.