CINXE.COM
DOI - JACoW-ICALEPCS2017-THPHA161
<!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-2018 Generated by JPSP version v=27.2= 05 Dec 2017 vrws on 2018-02-10 at 15:32" /> <meta name="author" content="volker rw schaa@gsi de" /> <link rel="stylesheet" type="text/css" 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" type="text/javascript"></script> <script src="../html/en.js" type="text/javascript"></script> <script type="text/javascript">Hyphenator.config({remoteloading : false}); Hyphenator.run();</script> <meta name="citation_author" content="Fern谩ndez Adiego, Borja" /> <meta name="citation_author" content="Avinashkrishna, Bhimavarapu" /> <meta name="citation_author" content="Blanco Vi帽uela, Enrique" /> <meta name="citation_author" content="Darvas, D脙隆niel" /> <meta name="citation_author" content="Gaikwad, Yogesh" /> <meta name="citation_author" content="Lee, Gisik" /> <meta name="citation_author" content="Pedica, Riccardo" /> <meta name="citation_author" content="Prieto Diaz, Ignacio" /> <meta name="citation_author" content="Sallai, Gyula" /> <meta name="citation_author" content="Sreekuttan, Sailaraj" /> <meta name="citation_date" content="2018/01" /> <meta name="citation_publication_date" content="2018/01/01" /> <meta name="citation_title" content="Applying Model Checking to Critical PLC Applications: An ITER Case Study" /> <meta name="citation_publisher" content="JACOW, Geneva, Switzerland" /> <meta name="citation_firstpage" content="1792" /> <meta name="citation_lastpage" content="1796" /> <meta name="citation_doi" content="10.18429/JACoW-ICALEPCS2017-THPHA161" /> <meta name="citation_isbn" content="978-3-95450-193-9" /> <meta name="citation_keywords" content="ion, PLC, SCADA, controls, software" /> <meta name="citation_language" content="en" /> <meta name="citation_conference_title" content="16th Int. Conf. on Accelerator and Large Experimental Control Systems (ICALEPCS'17), Barcelona, Spain, 8-13 October 2017" /> <meta name="citation_pdf_url" content="http://jacow.org/icalepcs2017/papers/thpha161.pdf" /> <meta name="DC.creator" content="Fern谩ndez Adiego, Borja" /> <meta name="DC.creator" content="Avinashkrishna, Bhimavarapu" /> <meta name="DC.creator" content="Blanco Vi帽uela, Enrique" /> <meta name="DC.creator" content="Darvas, D脙隆niel" /> <meta name="DC.creator" content="Gaikwad, Yogesh" /> <meta name="DC.creator" content="Lee, Gisik" /> <meta name="DC.creator" content="Pedica, Riccardo" /> <meta name="DC.creator" content="Prieto Diaz, Ignacio" /> <meta name="DC.creator" content="Sallai, Gyula" /> <meta name="DC.creator" content="Sreekuttan, Sailaraj" /> <meta name="DC.issued" content="meta_cit_date" /> <meta name="dcterms:issued" content="2018" /> <meta name="DC.title" content="Applying Model Checking to Critical PLC Applications: An ITER Case Study" /> <meta name="DC.publisher" content="JACOW, Geneva, Switzerland" /> <meta name="DC.citation.spage" content="1792" /> <meta name="DC.citation.epage" content="1796" /> <meta name="DC:identifier" content="info:doi/10.18429/JACoW-ICALEPCS2017-THPHA161" /> <meta name="dcterms:isPartOf" content="urn:ISBN:978-3-95450-193-9" /> <meta name="DC.subject" content="ion, PLC, SCADA, controls, software" /> <meta name="citation_language" content="en" /> <meta name="dcterms:bibliographicCitation" content="16th Int. Conf. on Accelerator and Large Experimental Control Systems (ICALEPCS'17), Barcelona, Spain, 8-13 October 2017" /> <meta name="DC.identifier" content="http://jacow.org/icalepcs2017/papers/thpha161.pdf" /> <title>DOI - JACoW-ICALEPCS2017-THPHA161</title> </head> <body> <a href="http://jacow.org"><img src="../im0ges/jacowheader.jpg" width="480" height="60" alt="JACoW logo" /></a> <h1>Joint Accelerator Conferences Website</h1> <p class="intro">The Joint Accelerator Conferences Website (<a href="http://jacow.org">JACoW</a>) is an international collaboration that publishes the proceedings of accelerator conferences held around the world.</p> <hr /> <div><span class="doiheader"><a href="http://jacow.org/icalepcs2017/papers/thpha161.pdf">https://doi.org/10.18429/JACoW-ICALEPCS2017-THPHA161</a></span></div> <div> <table class="doitabledef"> <tr class="tablerow"> <td class="fieldgrp">Title</td> <td class="fieldhigh">Applying Model Checking to Critical PLC Applications: An ITER Case Study</td> </tr> <tr class="tablerow"> <td class="fieldkey">Authors</td> <td class="datarow"> <ul> <li><span class="author_cl"><strong>B. Fernández Adiego</strong>, E. Blanco Viñuela, D. Darvas</span><br /> CERN, Geneva, Switzerland</li> <li><span class="author_cl">B. Avinashkrishna, Y.C. Gaikwad, S. Sreekuttan</span><br /> Tata Consultancy Services, Pune, India</li> <li><span class="author_cl">G.S. Lee</span><br /> Mobiis Co., Ltd., Seoul, Republic of Korea</li> <li><span class="author_cl">R. Pedica</span><br /> Vitrociset s.p.a, Roma, Italy</li> <li><span class="author_cl">I. Prieto Diaz</span><br /> IBERINCO, Madrid, Spain</li> <li><span class="author_cl">Gy. Sallai</span><br /> BUTE, Budapest, Hungary</li> </ul> </td> </tr> <tr class="tablerow"> <td class="fieldkey">Abstract</td> <td> <span class="abstract hyphenate jtext" lang="en">The development of critical systems requires the application of verification techniques in order to guarantee that the requirements are met in the system. Standards like IEC 61508 provide guidelines and recommend the use of formal methods for that purpose. The ITER Interlock Control System has been designed to protect the tokamak and its auxiliary systems from failures of the components or incorrect machine operation. ITER has developed a method to assure that some critical operator commands have been correctly received and executed in the PLC (Programmable Logic Controller). The implementation of the method in a PLC program is a critical part of the interlock system. A methodology designed at CERN has been applied to verify this PLC program. The methodology is the result of 5 years of research in the applicability of model checking to PLC programs. A proof-of-concept tool called PLCverif implements this methodology. This paper presents the challenges and results of the ongoing collaboration between CERN and ITER on formal verification of critical PLC programs.</span> </td> </tr> <tr class="tablerow"> <td class="fieldkey">Paper</td> <td class="datarow">download <a href="http://jacow.org/icalepcs2017/papers/thpha161.pdf" target="pdf">THPHA161.PDF</a> [0.161 MB / 5 pages]</td> </tr> <tr class="tablerow"> <td class="fieldkey">Poster</td> <td class="datarow">download <a href="http://jacow.org/icalepcs2017/posters/thpha161_poster.pdf" target="pdf">THPHA161_POSTER.PDF</a> [0.457 MB]</td> </tr> <tr class="tablerow"> <td class="fieldkey">Export</td> <td class="datarow">download ※ <a href="../export/THPHA161-bib.htm" target="exp">BibTeX</a> ※ <a href="../export/THPHA161-tex.htm" target="exp"> LaTeX</a> ※ <a href="../export/THPHA161-txt.htm" target="exp">Text/Word</a> ※ <a href="../export/THPHA161-ris.htm" target="exp">RIS</a> ※ <a href="../export/THPHA161.xml" target="exp">EndNote</a></td> </tr> <tr class="tablerow"> <td class="fieldgrp">Conference</td> <td class="fieldhigh">ICALEPCS2017, Barcelona, Spain</td> </tr> <tr class="tablerow"> <td class="fieldkey">Series</td> <td class="datarow">International Conference on Accelerator and Large Experimental Control Systems (16th)</td> </tr> <tr class="tablerow"> <td class="fieldkey">Proceedings</td> <td class="datarow">Link to full <a href="http://jacow.org/icalepcs2017/" target="pdf">ICALEPCS2017 Proccedings</a></td> </tr> <tr class="tablerow"> <td class="fieldkey">Session</td> <td class="datarow">Poster Session</td> </tr> <tr class="tablerow"> <td class="fieldkey">Date</td> <td class="datarow">12-Oct-17 16:45–19:00</td> </tr> <tr class="tablerow"> <td class="fieldkey">Main Classification</td> <td class="datarow">Software Technology Evolution</td> </tr> <tr class="tablerow"> <td class="fieldkey">Keywords</td> <td class="datarow">ion, PLC, SCADA, controls, software</td> </tr> <tr class="tablerow"> <td class="fieldgrp">Publisher</td> <td class="fieldhigh">JACoW, Geneva, Switzerland</td> </tr> <tr class="tablerow"> <td class="fieldkey">Editors</td> <td class="datarow">Volker RW Schaa (GSI, Darmstadt, Germany); Isidre Costa (ALBA-CELLS, Cerdanyola del Vall脙篓s, Spain); David Fern脙隆ndez (ALBA-CELLS, Cerdanyola del Vall脙篓s, Spain); 脙聯scar Matilla (ALBA-CELLS, Cerdanyola del Vall脙篓s, Spain)</td> </tr> <tr class="tablerow"> <td class="fieldkey">ISBN</td> <td class="datarow">978-3-95450-193-9</td> </tr> <tr class="tablerow"> <td class="fieldkey">Published</td> <td class="datarow">January 2018</td> </tr> <tr class="tablerow"> <td class="fieldkey">Copyright</td> <td class="datarow"> <table> <tr><td>Copyright © 2018 by JACoW, Geneva, Switzerland</td><td> </td> <td rowspan="2"><img src="../im0ges/ccby-88x31.png" width="88" height="31" alt="CC-BY Creative Commons License" /></td> </tr> <tr><td>cc <a href="https://creativecommons.org/licenses/by/3.0/">Creative Commons Attribution 3.0</a></td><td> </td> </tr> </table> </td> </table> </div> </body> </html>