CINXE.COM
DOI - JACoW-ICALEPCS2023-TUPDP001
<!DOCTYPE html> <html lang="en"> <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <meta name="keywords" content="doi, conference, proceedings" /> <meta name="generator" content="copyright 2015-2024 Generated by JPSP version v=36.2=(pre 36.2)漏22 Oct 2023 vrws on 2024-01-30 at 02:45" /> <meta name="generator" content="JPSP script name 禄H:/JACoW/JPSP/spmsbatchU.pl芦 modification date 禄Tue Jan 23 17:03:27 2024芦" /> <meta name="author" content="volker rw schaa@gsi de" /> <link rel="stylesheet" href="../html/doi.css" /> <link rel="shortcut icon" href="../im0ges/favicon.ico" /> <link rel="icon" href="../im0ges/favicon_ani.gif" type="image/gif" /> <script src="../html/Hyphenator.js"></script> <script src="../html/en.js"></script> <script type="text/javascript">Hyphenator.config({remoteloading : false}); Hyphenator.run();</script> <meta name="citation_title" content="Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code" /> <meta name="citation_author" content="Lopez-Miguel, Ignacio D." /> <meta name="citation_author" content="Betz, Christine" /> <meta name="citation_author" content="Blanco Vi帽uela, Enrique" /> <meta name="citation_author" content="Fern谩ndez Adiego, Borja" /> <meta name="citation_author" content="Salinas, Matias" /> <meta name="citation_date" content="2024/01" /> <meta name="citation_publication_date" content="2024/01/01" /> <meta name="citation_publisher" content="JACOW Publishing, Geneva, Switzerland" /> <meta name="citation_firstpage" content="467" /> <meta name="citation_lastpage" content="472" /> <meta name="citation_doi" content="10.18429/JACoW-ICALEPCS2023-TUPDP001" /> <meta name="citation_isbn" content="978-3-95450-238-7" /> <meta name="citation_issn" content="2226-0358" /> <meta name="citation_keywords" content="PLC, software, controls, operation, GUI" /> <meta name="citation_language" content="en" /> <meta name="citation_conference_title" content="19th International Conference on Accelerator and Large Experimental Physics Control Systems (ICALEPCS'23), Cape Town, South Africa, 09-13 October 2023" /> <meta name="citation_pdf_url" content="https://jacow.org/icalepcs2023/papers/tupdp001.pdf" /> <meta name="DC.creator" content="Lopez-Miguel, Ignacio D." /> <meta name="DC.creator" content="Betz, Christine" /> <meta name="DC.creator" content="Blanco Vi帽uela, Enrique" /> <meta name="DC.creator" content="Fern谩ndez Adiego, Borja" /> <meta name="DC.creator" content="Salinas, Matias" /> <meta name="DC.issued" content="2024/01" /> <meta name="dcterms:issued" content="2024" /> <meta name="DC.title" content="Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code" /> <meta name="DC.publisher" content="JACOW Publishing, Geneva, Switzerland" /> <meta name="DC.citation.spage" content="467" /> <meta name="DC.citation.epage" content="472" /> <meta name="DC:identifier" content="info:doi/10.18429/JACoW-ICALEPCS2023-TUPDP001" /> <meta name="dcterms:isPartOf" content="urn:ISSN:2226-0358" /> <meta name="dcterms:isPartOf" content="urn:ISBN:978-3-95450-238-7" /> <meta name="DC.subject" content="PLC, software, controls, operation, GUI" /> <meta name="citation_language" content="en" /> <meta name="dcterms:bibliographicCitation" content="19th International Conference on Accelerator and Large Experimental Physics Control Systems (ICALEPCS'23), Cape Town, South Africa, 09-13 October 2023" /> <meta name="DC.identifier" content="https://jacow.org/icalepcs2023/papers/tupdp001.pdf" /> <title>DOI - JACoW-ICALEPCS2023-TUPDP001</title> </head> <body> <a href="https://www.jacow.org"><img src="../im0ges/jacowheader.jpg" width="480" height="60" alt="JACoW logo" /></a> <h1>Journals of Accelerator Conferences Website (JACoW)</h1> <p class="intro">'Journal of Accelerator Conferences Website' (<a href="https://www.jacow.org">JACoW</a>) is a publisher in Geneva, Switzerland that publishes the proceedings of accelerator conferences held around the world by an international collaboration of editors.</p> <hr /> <div><span class="doiheader"><a href="https://jacow.org/icalepcs2023/papers/tupdp001.pdf">https://doi.org/10.18429/JACoW-ICALEPCS2023-TUPDP001</a></span></div> <div> <table class="doitabledef"> <tr class="tablerow"> <td class="fieldgrp">Title</td> <td class="fieldhigh">Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code</td> </tr> <tr class="tablerow"> <td class="fieldkey">Authors</td> <td class="datarowleft"> <ul> <li><span class="author_cl"><strong>I.D. Lopez-Miguel</strong></span><br /> IAP TUW, Wien, Austria</li> <li><span class="author_cl">C. Betz, M. Salinas</span><br /> GSI, Darmstadt, Germany</li> <li><span class="author_cl"><span class="tooltip presenter">E. Blanco Vinuela<span class="pr-text presentertxt">presenter</span></span>, B. Fern谩ndez Adiego</span><br /> CERN, Meyrin, Switzerland</li> </ul> </td> </tr> <tr class="tablerow"> <td class="fieldkey">Abstract</td> <td> <span class="abstract hyphenate jtext" lang="en">Formal verification techniques are widely used in critical industries to minimize software flaws. However, despite the benefits and recommendations of the functional safety standards, such as IEC 61508 and IEC 61511, formal verification is not yet a common practice in the process industry and large scientific installations. This is mainly due to its complexity and the need for formal methods experts. At CERN, the PLCverif tool was developed to verify PLC programs formally. Although PLCverif hides most of the complexity of using formal methods and removes barriers to formally verifying PLC programs, engineers trying to verify their developments still encounter different obstacles. These challenges include the formalization of program specifications or the creation of formal models. This paper discusses how to overcome these obstacles by proposing a collaboration model that effectively allows the verification of critical PLC programs and promotes knowledge transfer between organizations. By providing a simpler and more accessible way to carry out formal verification, tools like PLCverif can play a crucial role in achieving this goal. The collaboration model splits the specification, development, and verification tasks between organizations. This approach is illustrated through a case study between GSI and CERN. </span> </td> </tr> <tr class="tablerow"> <td class="fieldkey">Paper</td> <td class="datarow">download <a href="https://jacow.org/icalepcs2023/papers/tupdp001.pdf" target="pdf">TUPDP001.PDF</a> [0.169 MB / 6 pages]</td> </tr> <tr class="tablerow"> <td class="fieldkey">Poster</td> <td class="datarow">download <a href="https://jacow.org/icalepcs2023/posters/tupdp001_poster.pdf" target="pdf">TUPDP001_POSTER.PDF</a> [0.739 MB]</td> </tr> <tr class="tablerow"> <td class="fieldkey">Cite</td> <td class="datarow">download ※ <a href="../export/TUPDP001-bib.htm" target="exp">BibTeX</a> ※ <a href="../export/TUPDP001-tex.htm" target="exp"> LaTeX</a> ※ <a href="../export/TUPDP001-txt.htm" target="exp">Text/Word</a> ※ <a href="../export/TUPDP001-ris.htm" target="exp">RIS</a> ※ <a href="../export/TUPDP001.xml" target="exp">EndNote</a></td> </tr> <tr class="tablerow"> <td class="fieldgrp">Conference</td> <td class="fieldhigh"><a href="https://jacow.org/icalepcs2023/" target="pdf">ICALEPCS2023</a></td> </tr> <tr class="tablerow"> <td class="fieldkey">Series</td> <td class="datarow">International Conference on Accelerator and Large Experimental Physics Control Systems (19th)</td> </tr> <tr class="tablerow"> <td class="fieldkey">Location</td> <td class="datarow">Cape Town, South Africa</td> </tr> <tr class="tablerow"> <td class="fieldkey">Date</td> <td class="datarow">09-13 October 2023</td> </tr> <tr class="tablerow"> <td class="fieldgrp">Publisher</td> <td class="fieldhigh"><a href="https://www.jacow.org" target="pdf">JACoW Publishing, Geneva, Switzerland</a></td> </tr> <tr class="tablerow"> <td class="fieldkey">Editorial Board</td> <td class="datarow">Volker RW Schaa (GSI, Darmstadt, Germany); Andy G枚tz (ESRF, Grenoble, France); Johan Venter (SARAO, Cape Town, South Africa); Karen White (SNS, Oak Ridge, TN, USA); Marie Robichon (ESRF, Grenoble, France); Vivienne Rowland (SARAO, Cape Town, South Africa)</td> </tr> <tr class="tablerow"> <td class="fieldkey" nowrap>Online ISBN</td> <td class="datarow">978-3-95450-238-7</td> </tr> <tr class="tablerow"> <td class="fieldkey" nowrap>Online ISSN</td> <td class="datarow">2226-0358</td> </tr> <tr class="tablerow"> <td class="fieldkey">Received</td> <td class="datarow">03 October 2023</td> </tr> <tr class="tablerow"> <td class="fieldkey">Accepted</td> <td class="datarow">20 November 2023</td> </tr> <tr class="tablerow"> <td class="fieldkey">Issued/td> <td class="datarow">19 December 2023</td> </tr> <tr class="tablerow"> <td class="fieldkey">DOI</td> <td class="datarow"><span style="font-family:'Liberation Mono'; font-size:12pt;">doi:10.18429/JACoW-ICALEPCS2023-TUPDP001</span></td> </tr> <tr class="tablerow"> <td class="fieldkey">Pages</td> <td class="datarow">467-472</td> </tr> <tr class="tablerow"> <td class="fieldkey">Copyright</td> <td class="datarow"> <table> <tr><td><span class="abstract hyphenate jtext" lang="en"><a href="https://creativecommons.org/licenses/by/3.0/"><img alt="Creative Commons CC logo" src="../im0ges/cc.png" style="float: left; margin: 10px" height="30"></a><i>Published by JACoW Publishing under the terms of the <a href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International</a> license. Any further distribution of this work must maintain attribution to the author(s), the published article's title, publisher, and DOI.</i></span></td> </tr> </table> </td> </table> </div> </body> </html>