  As a general trend in industrial robotics, an increasing number of safety
functions are being developed or re-engineered to be handled in software rather
than by physical hardware such as safety relays or interlock circuits. This
trend reinforces the importance of supplementing traditional, input-based
testing and quality procedures which are widely used in industry today, with
formal verification and model-checking methods. To this end, this paper focuses
on a representative safety-critical system in an ABB industrial paint robot,
namely the High-Voltage electrostatic Control system (HVC). The practical
convergence of the high-voltage produced by the HVC, essential for safe
operation, is formally verified using a novel and general co-verification
framework where hardware and software models are related via platform mappings.
This approach enables the pragmatic combination of highly diverse and
specialised tools. The paper's main contribution includes details on how
hardware abstraction and verification results can be transferred between tools
in order to verify system-level safety properties. It is noteworthy that the
HVC application considered in this paper has a rather generic form of a
feedback controller. Hence, the co-verification framework and experiences
reported here are also highly relevant for any cyber-physical system tracking a
setpoint reference.
