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.
|Title of host publication||Formal Methods|
|Subtitle of host publication||Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Proceedings|
|Editors||Gustavo Carvalho, Volker Stolz|
|Number of pages||19|
|Publication status||Published - 19 Nov 2020|
|Event||23rd Brazilian Symposium on Formal Methods, SBMF 2020 - Ouro Preto, Brazil|
Duration: 25 Nov 2020 → 27 Nov 2020
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||23rd Brazilian Symposium on Formal Methods, SBMF 2020|
|Period||25/11/20 → 27/11/20|
Bibliographical noteFunding 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.
© 2020, The Author(s).
- Formal verification
- High Voltage Controller (HVC)
- Industrial robots
- Model checking