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

doi:10.1007/978-3-030-63882-5_4

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	Formal Methods
Subtitle of host publication	Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Proceedings
Editors	Gustavo Carvalho, Volker Stolz
Publisher	Springer
Pages	45-63
Number of pages	19
ISBN (Print)	9783030638818
DOIs	https://doi.org/10.1007/978-3-030-63882-5_4
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

Publication series

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

Conference

Conference	23rd Brazilian Symposium on Formal Methods, SBMF 2020
Country/Territory	Brazil
City	Ouro Preto
Period	25/11/20 → 27/11/20

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).

Keywords

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

Access to Document

10.1007/978-3-030-63882-5_4

Murray2020_Chapter_SafetyAssuranceOfAHighVoltageC
c The Author(s) 2020
Final published version, 3.02 MBLicence: CC BY

Cite this

Murray, Y., Anisi, D. A., Sirevåg, M., Ribeiro, P., & Hagag, R. S. (2020). Safety assurance of a high voltage controller for an industrial robotic system. In G. Carvalho, & V. Stolz (Eds.), Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Proceedings (pp. 45-63). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12475 LNCS). Springer. https://doi.org/10.1007/978-3-030-63882-5_4

Murray, Yvonne ; Anisi, David A. ; Sirevåg, Martin et al. / Safety assurance of a high voltage controller for an industrial robotic system. Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Proceedings. editor / Gustavo Carvalho ; Volker Stolz. Springer, 2020. pp. 45-63 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4d23d2d5a58046af99cd3cec71e6a467,

title = "Safety assurance of a high voltage controller for an industrial robotic system",

abstract = "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.",

keywords = "Formal verification, High Voltage Controller (HVC), Industrial robots, Model checking",

author = "Yvonne Murray and Anisi, {David A.} and Martin Sirev{\aa}g and Pedro Ribeiro and Hagag, {Rabah Saleh}",

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: {\textcopyright} 2020, The Author(s).; 23rd Brazilian Symposium on Formal Methods, SBMF 2020 ; Conference date: 25-11-2020 Through 27-11-2020",

year = "2020",

month = nov,

day = "19",

doi = "10.1007/978-3-030-63882-5_4",

language = "English",

isbn = "9783030638818",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "45--63",

editor = "Gustavo Carvalho and Volker Stolz",

booktitle = "Formal Methods",

address = "Germany",

}

Murray, Y, Anisi, DA, Sirevåg, M, Ribeiro, P & Hagag, RS 2020, Safety assurance of a high voltage controller for an industrial robotic system. in G Carvalho & V Stolz (eds), Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12475 LNCS, Springer, pp. 45-63, 23rd Brazilian Symposium on Formal Methods, SBMF 2020, Ouro Preto, Brazil, 25/11/20. https://doi.org/10.1007/978-3-030-63882-5_4

Safety assurance of a high voltage controller for an industrial robotic system. / Murray, Yvonne; Anisi, David A.; Sirevåg, Martin et al.
Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Proceedings. ed. / Gustavo Carvalho; Volker Stolz. Springer, 2020. p. 45-63 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12475 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Murray, Yvonne

AU - Anisi, David A.

AU - Sirevåg, Martin

AU - Ribeiro, Pedro

AU - Hagag, Rabah Saleh

N1 - 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).

PY - 2020/11/19

Y1 - 2020/11/19

N2 - 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.

AB - 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.

KW - Formal verification

KW - High Voltage Controller (HVC)

KW - Industrial robots

KW - Model checking

UR - http://www.scopus.com/inward/record.url?scp=85097278986&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-63882-5_4

DO - 10.1007/978-3-030-63882-5_4

M3 - Conference contribution

AN - SCOPUS:85097278986

SN - 9783030638818

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 45

EP - 63

BT - Formal Methods

A2 - Carvalho, Gustavo

A2 - Stolz, Volker

PB - Springer

T2 - 23rd Brazilian Symposium on Formal Methods, SBMF 2020

Y2 - 25 November 2020 through 27 November 2020

ER -

Murray Y, Anisi DA, Sirevåg M, Ribeiro P, Hagag RS. Safety assurance of a high voltage controller for an industrial robotic system. In Carvalho G, Stolz V, editors, Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Proceedings. Springer. 2020. p. 45-63. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-63882-5_4

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

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Cite this