Safety assurance of a high voltage controller for an industrial robotic system

Yvonne Murray*, David A. Anisi, Martin Sirevåg, Pedro Ribeiro, Rabah Saleh Hagag

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Due to the risk of discharge sparks and ignition, there are strict rules concerning the safety of high voltage electrostatic systems used in industrial painting robots. In order to assure that the system fulfils its safety requirements, formal verification is an important tool to supplement traditional testing and quality assurance procedures. The work in this paper presents formal verification of the most important safety functions of a high voltage controller. The controller has been modelled as a finite state machine, which was formally verified using two different model checking software tools; Simulink Design Verifier and RoboTool. Five safety critical properties were specified and formally verified using the two tools. Simulink was chosen as a low-threshold entry point since MathWorks products are well known to most practitioners. RoboTool serves as a software tool targeted towards model checking, thus providing more advanced options for the more experienced user. The comparative study and results show that all properties were successfully verified. The verification times in both tools were in the order of a few minutes, which was within the acceptable time limit for this particular application.

Original languageEnglish
Title of host publicationFormal Methods
Subtitle of host publicationFoundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Proceedings
EditorsGustavo Carvalho, Volker Stolz
Number of pages19
ISBN (Print)9783030638818
Publication statusPublished - 19 Nov 2020
Event23rd Brazilian Symposium on Formal Methods, SBMF 2020 - Ouro Preto, Brazil
Duration: 25 Nov 202027 Nov 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12475 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd Brazilian Symposium on Formal Methods, SBMF 2020
CityOuro Preto

Bibliographical note

Funding Information:
The research presented in this paper has received funding from the Norwegian Research Council, SFI Offshore Mechatronics, project number 237896. Pedro Ribeiro is funded by the UK EPSRC under grant EP/M025756/1.

Publisher Copyright:
© 2020, The Author(s).


  • Formal verification
  • High Voltage Controller (HVC)
  • Industrial robots
  • Model checking

Cite this