CINXE.COM
Applying model checking to critical PLC applications - CERN Document Server
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> <!--[if IEMobile 7]><html class="iem7" xmlns="http://www.w3.org/1999/xhtml" lang="it" xml:lang="it" xmlns:og="http://ogp.me/ns#" xmlns:fb="http://ogp.me/ns/fb#"><![endif]--> <!--[if lte IE 6]><html class="ie6 ie6-7 ie6-8" xmlns="http://www.w3.org/1999/xhtml" lang="it" xml:lang="it" xmlns:og="http://ogp.me/ns#" xmlns:fb="http://ogp.me/ns/fb#"><![endif]--> <!--[if (IE 7)&(!IEMobile)]><html class="ie7 ie6-7 ie6-8" xmlns="http://www.w3.org/1999/xhtml" lang="it" xml:lang="it" xmlns:og="http://ogp.me/ns#" xmlns:fb="http://ogp.me/ns/fb#"><![endif]--> <!--[if IE 8]><html class="ie8 ie6-8" xmlns="http://www.w3.org/1999/xhtml" lang="it" xml:lang="it" xmlns:og="http://ogp.me/ns#" xmlns:fb="http://ogp.me/ns/fb#"><![endif]--> <!--[if (gte IE 9)|(gt IEMobile 7)]><!--><html xmlns="http://www.w3.org/1999/xhtml" lang="it" xml:lang="it" xmlns:og="http://ogp.me/ns#" xmlns:fb="http://ogp.me/ns/fb#"><!--<![endif]--> <head> <title>Applying model checking to critical PLC applications - CERN Document Server</title> <link href='https://framework.web.cern.ch/framework/2.0/fonts/PTSansWeb/PTSansWeb.css' rel='stylesheet' type='text/css' /> <link rel="stylesheet" href="https://cds.cern.ch/img/invenio.css?v=20141127" type="text/css" /> <link rel="stylesheet" href="https://cds.cern.ch/img/cern_theme/css/cern_theme.css?v=20141127" type="text/css" /> <link rel="stylesheet"href="/css/font-awesome.min.css"> <meta http-equiv="X-UA-Compatible" content="IE=Edge"/> <link rel="stylesheet" href="https://cds.cern.ch/img/cern_toolbar/css/toolbar.css" type="text/css" /> <!--[if lt IE 8]> <link href="https://cds.cern.ch/img/cern_toolbar/css/toolbar-ie.css" rel="stylesheet" type="text/css"> <![endif]--> <!--[if lt IE 8]> <link rel="stylesheet" type="text/css" href="https://cds.cern.ch/img/invenio-ie7.css" /> <![endif]--> <!--[if gt IE 8]> <style type="text/css">div.restrictedflag {filter:none;}</style> <![endif]--> <link rel="canonical" href="https://cds.cern.ch/record/2305319" /> <link rel="alternate" hreflang="el" href="https://cds.cern.ch/record/2305319?ln=el" /> <link rel="alternate" hreflang="fr" href="https://cds.cern.ch/record/2305319?ln=fr" /> <link rel="alternate" hreflang="bg" href="https://cds.cern.ch/record/2305319?ln=bg" /> <link rel="alternate" hreflang="zh-TW" href="https://cds.cern.ch/record/2305319?ln=zh_TW" /> <link rel="alternate" hreflang="pt" href="https://cds.cern.ch/record/2305319?ln=pt" /> <link rel="alternate" hreflang="no" href="https://cds.cern.ch/record/2305319?ln=no" /> <link rel="alternate" hreflang="hr" href="https://cds.cern.ch/record/2305319?ln=hr" /> <link rel="alternate" hreflang="ca" href="https://cds.cern.ch/record/2305319?ln=ca" /> <link rel="alternate" hreflang="de" href="https://cds.cern.ch/record/2305319?ln=de" /> <link rel="alternate" hreflang="it" href="https://cds.cern.ch/record/2305319?ln=it" /> <link rel="alternate" hreflang="zh-CN" href="https://cds.cern.ch/record/2305319?ln=zh_CN" /> <link rel="alternate" hreflang="sv" href="https://cds.cern.ch/record/2305319?ln=sv" /> <link rel="alternate" hreflang="sk" href="https://cds.cern.ch/record/2305319?ln=sk" /> <link rel="alternate" hreflang="en" href="https://cds.cern.ch/record/2305319?ln=en" /> <link rel="alternate" hreflang="pl" href="https://cds.cern.ch/record/2305319?ln=pl" /> <link rel="alternate" hreflang="ru" href="https://cds.cern.ch/record/2305319?ln=ru" /> <link rel="alternate" hreflang="ka" href="https://cds.cern.ch/record/2305319?ln=ka" /> <link rel="alternate" hreflang="ja" href="https://cds.cern.ch/record/2305319?ln=ja" /> <link rel="alternate" hreflang="es" href="https://cds.cern.ch/record/2305319?ln=es" /> <link rel="alternate" type="application/rss+xml" title="CERN Document Server RSS" href="/rss?ln=it" /> <link rel="search" type="application/opensearchdescription+xml" href="https://cds.cern.ch/opensearchdescription" title="CERN Document Server" /> <link rel="unapi-server" type="application/xml" title="unAPI" href="https://cds.cern.ch/unapi" /> <link rel="apple-touch-icon" href="/apple-touch-icon.png"/> <link rel="apple-touch-icon-precomposed" href="/apple-touch-icon-precomposed.png"/> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <meta http-equiv="Content-Language" content="it" /> <meta name="description" content="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. Fernández Adiego, Borja; Avinashkrishna, Bhimavarapu; Blanco Viñuela, Enrique; Darvas, Daniel; Gaikwad, Yogesh; Lee, Gisik; Pedica, Riccardo; Prieto Diaz, Ignacio; Sallai, Gyula; Sreekuttan, Sailaraj" /> <meta name="keywords" content="ion, PLC, SCADA, controls, software" /> <script type="text/javascript" src="https://cds.cern.ch/js/jquery.min.js"></script> <!-- WebNews CSS library --> <link rel="stylesheet" href="https://cds.cern.ch/img/webnews.css" type="text/css" /> <!-- WebNews JS library --> <script type="text/javascript" src="https://cds.cern.ch/js/webnews.js?v=20131009"></script> <meta property="fb:app_id" content="137353533001720"/> <script type="text/x-mathjax-config"> MathJax.Hub.Config({ tex2jax: {inlineMath: [['$','$']], processEscapes: true}, showProcessingMessages: false, messageStyle: "none" }); </script> <script src="/MathJax/MathJax.js?config=TeX-AMS_CHTML" type="text/javascript"> </script> <!-- GoogleScholar --> <meta content="JACoW : Applying model checking to critical PLC applications : An ITER case study" name="citation_title" /> <meta content="Fernández Adiego, Borja" name="citation_author" /> <meta content="Blanco Viñuela, Enrique" name="citation_author" /> <meta content="Avinashkrishna, Bhimavarapu" name="citation_author" /> <meta content="Sreekuttan, Sailaraj" name="citation_author" /> <meta content="Pedica, Riccardo" name="citation_author" /> <meta content="Sallai, Gyula" name="citation_author" /> <meta content="Gaikwad, Yogesh" name="citation_author" /> <meta content="Darvas, Daniel" name="citation_author" /> <meta content="Lee, Gisik" name="citation_author" /> <meta content="Prieto Diaz, Ignacio" name="citation_author" /> <meta content="10.18429/JACoW-ICALEPCS2017-THPHA161" name="citation_doi" /> <meta content="THPHA161" name="citation_firstpage" /> <meta content="2018" name="citation_publication_date" /> <meta name="citation_online_date" content="2018/02/22"> <meta content="10.18429/JACoW-ICALEPCS2017-THPHA161" name="citation_doi" /> <meta name="citation_pdf_url" content="https://cds.cern.ch/record/2305319/files/thpha161.pdf" /> <!-- OpenGraph --> <meta content="JACoW" property="og:title" /> <meta content="An ITER case study" property="og:title" /> <meta content="Applying model checking to critical PLC applications" property="og:title" /> <meta content="website" property="og:type" /> <meta content="website" property="og:type" /> <meta content="https://cds.cern.ch/record/2305319" property="og:url" /> <meta content="CERN Document Server" property="og:site_name" /> <meta content="JACoW" property="og:description" /> <meta content="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." property="og:description" /> <!-- Twitter Card --> <meta content="summary" name="twitter:card" /> <meta content="summary" name="twitter:card" /> <style></style> </head> <body class="CERN32Document32Server search" lang="it"> <!-- toolbar starts --> <div id="cern-toolbar"> <h1><a href="http://cern.ch" title="CERN">CERN <span>Accelerating science</span></a></h1> <ul> <li class="cern-accountlinks"><a class="cern-account" href="https://cds.cern.ch/youraccount/login?ln=it&referer=https%3A//cds.cern.ch/record/2305319%3Fln%3Dit" title="Sign in to your CERN account">Sign in</a></li> <li><a class="cern-directory" href="http://cern.ch/directory" title="Search CERN resources and browse the directory">Directory</a></li> </ul> </div> <!-- toolbar ends --> <!-- Nav header starts--> <div role="banner" class="clearfix" id="header"> <div class="header-inner inner"> <hgroup class="clearfix"> <h2 id="site-name"> <a rel="home" title="Home" href="/"><span>CERN Document Server</span></a> </h2> <h3 id="site-slogan">Access articles, reports and multimedia content in HEP</h3> </hgroup><!-- /#name-and-slogan --> <div role="navigation" id="main-navigation" class="cdsmenu"> <h2 class="element-invisible">Main menu</h2><ul class="links inline clearfix"> <li class="menu-386 first active-trail"><a class="active-trail" href="https://cds.cern.ch/?ln=it">Cerca</a></li> <li class="menu-444 "><a class="" title="" href="https://cds.cern.ch/submit?ln=it">Sottometti</a></li> <li class="menu-426 "><a class="" href="https://cds.cern.ch/help/?ln=it">Aiuto</a></li> <li class="leaf hassubcdsmenu"> <a hreflang="en" class="header" href="https://cds.cern.ch/youraccount/display?ln=it">Personalizza</a> <ul class="subsubcdsmenu"><li><a href="https://cds.cern.ch/youralerts/list?ln=it">I tuoi avvisi</a></li><li><a href="https://cds.cern.ch/yourbaskets/display?ln=it">I tuoi cestini</a></li><li><a href="https://cds.cern.ch/yourcomments?ln=it">Your comments</a></li><li><a href="https://cds.cern.ch/youralerts/display?ln=it">Le tue ricerche</a></li></ul></li> </ul> </div> </div> </div> <!-- Nav header ends--> <table class="navtrailbox"> <tr> <td class="navtrailboxbody"> <a href="/?ln=it" class="navtrail">Pagina principale</a> > Applying model checking to critical PLC applications </td> </tr> </table> </div> <div class="pagebody"><div class="pagebodystripemiddle"> <div class="detailedrecordbox"> <div class="detailedrecordtabs"> <div> <ul class="detailedrecordtabs"><li class="on first"><a href="/record/2305319/?ln=it">Informazioni </a></li><li class=""><a href="/record/2305319/files?ln=it">File </a></li></ul> <div id="tabsSpacer" style="clear:both;height:0px"> </div></div> </div> <div class="detailedrecordboxcontent"> <div class="top-left-folded"></div> <div class="top-right-folded"></div> <div class="inside"> <!--<div style="height:0.1em;"> </div> <p class="notopgap"> </p>--> <abbr class="unapi-id" title="2305319"></abbr> <style type="text/css"> <!-- ul.detailedrecordtabs li.on a{background-color:#4D94CC;color:#fff !important;border-bottom:1px solid #4D94CC!important;} div.detailedrecordboxcontent {padding-top:0px !important;} --> </style> <table class="formatRecordTableFullWidth" > <tr> <td class="formatRecordHeader" style="background-image: url('https://cds.cern.ch/img/journals.jpg');" colspan="2"> <!--YTD: record may have more than one 690C.a tag--> <a style="color:#fff;text-decoration:none" href="https://cds.cern.ch/collection/Published%20Articles">Published Articles</a> </td> </tr> <script type="text/javascript"> $( document ).ready(function() { $('.showAuthor').on('click', function() { var author = '<p>' + $(this).data('name') + '</p>'; var affiliation = $(this).data('affiliation') + '</br>'; var contribution = $(this).data('contribution') + '</br>'; $.magnificPopup.open({ items: { src: '<div id="ovelary-mathjax" class="overlay-white oc-content overlay-white-500">' + author + affiliation + contribution + '</div>', type: 'inline' }, callbacks: { open: function() { var div = document.getElementById("overlay-mathjax") MathJax.Hub.Queue(["Typeset", MathJax.Hub, div]); }, } }) }) }); </script> <tr><td class="formatRecordLabel"> Title </td><td style="padding-left:5px;"><b>Applying model checking to critical PLC applications : An ITER case study</b></td></tr> <tr><td class="formatRecordLabel"><span style="white-space:nowrap;"> Author(s) </span> </td><td style="padding-left:5px;"><a href="https://cds.cern.ch/search?f=author&p=Fern%C3%A1ndez%20Adiego%2C%20Borja&ln=it">Fernández Adiego, Borja</a> (CERN) ; <a href="https://cds.cern.ch/search?f=author&p=Avinashkrishna%2C%20Bhimavarapu&ln=it">Avinashkrishna, Bhimavarapu</a> (TCS, Madhapur) ; <a href="https://cds.cern.ch/search?f=author&p=Blanco%20Vi%C3%B1uela%2C%20Enrique&ln=it">Blanco Viñuela, Enrique</a> (CERN) ; <a href="https://cds.cern.ch/search?f=author&p=Darvas%2C%20Daniel&ln=it">Darvas, Daniel</a> (CERN) ; <a href="https://cds.cern.ch/search?f=author&p=Gaikwad%2C%20Yogesh&ln=it">Gaikwad, Yogesh</a> (TCS, Madhapur) ; <a href="https://cds.cern.ch/search?f=author&p=Lee%2C%20Gisik&ln=it">Lee, Gisik</a> (Mobiis Co. Ltd., Seoul) ; <a href="https://cds.cern.ch/search?f=author&p=Pedica%2C%20Riccardo&ln=it">Pedica, Riccardo</a> (Vitrociset, Rome) ; <a href="https://cds.cern.ch/search?f=author&p=Prieto%20Diaz%2C%20Ignacio&ln=it">Prieto Diaz, Ignacio</a> (IBERINCO, Madrid) ; <a href="https://cds.cern.ch/search?f=author&p=Sallai%2C%20Gyula&ln=it">Sallai, Gyula</a> (Budapest, Tech. U.) ; <a href="https://cds.cern.ch/search?f=author&p=Sreekuttan%2C%20Sailaraj&ln=it">Sreekuttan, Sailaraj</a> (TCS, Madhapur)</td></tr> <tr><td class="formatRecordLabel"> Publication </td><td style="padding-left:5px;">2018</td></tr> <tr><td class="formatRecordLabel"> Number of pages </td><td style="padding-left:5px;">5</td></tr> <tr><td class="formatRecordLabel"> In: </td><td style="padding-left:5px;"><a href="https://cds.cern.ch/record/2288115">16th International Conference on Accelerator and Large Experimental Physics Control Systems</a>, Barcelona, Spain, 8 - 13 Oct 2017, pp.THPHA161</td></tr> <tr><td class="formatRecordLabel"> DOI </td><td style="padding-left:5px;"><a href="http://dx.doi.org/10.18429/JACoW-ICALEPCS2017-THPHA161" title="DOI" target="_blank">10.18429/JACoW-ICALEPCS2017-THPHA161</a> <tr><td class="formatRecordLabel"> Subject category </td><td style="padding-left:5px;">Accelerators and Storage Rings</td></tr> <tr><td class="formatRecordLabel"> Abstract </td><td style="padding-left:5px;">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.</td></tr> <tr><td class="formatRecordLabel"> Copyright/License </td><td style="padding-left:5px;"><a href="http://creativecommons.org/licenses/by/3.0/">CC-BY-3.0</a></td></tr> </table> <br/>Corresponding record in: <a href="http://inspirehep.net/record/1656450">Inspire</a> <small> </small> <br/> <br/><br/><div align="right"><div style="padding-bottom:2px;padding-top:30px;"><span class="moreinfo" style="margin-right:10px;"> <a href="" class="moreinfo">Back to search</a> </span></div></div> <div class="bottom-left-folded"><div class="recordlastmodifiedbox" style="position:relative;margin-left:1px"> Record creato 2018-02-22, modificato l'ultima volta il 2018-02-23</div></div> <div class="bottom-right-folded" style="text-align:right;padding-bottom:2px;"> <span class="moreinfo" style="margin-right:10px;"><a href="/search?ln=it&p=recid%3A2305319&rm=wrd" class="moreinfo">Record simili</a></span></div> </div> </div> </div> <br/> <br /> <div class="detailedrecordminipanel"> <div class="top-left"></div><div class="top-right"></div> <div class="inside"> <div id="detailedrecordminipanelfile" style="width:33%;float:left;text-align:center;margin-top:0"> <div><small class="detailedRecordActions">Testo completo:</small> <br /><a href="/record/2305319/files/thpha161.pdf"><img style="border:none" src="/img/file-icon-text-34x48.gif" alt="Scarica documento" /><br />PDF</a><br /></div> </div> <div id="detailedrecordminipanelreview" style="width:30%;float:left;text-align:center"> </div> <div id="detailedrecordminipanelactions" style="width:36%;float:right;text-align:right;"> <ul class="detailedrecordactions"> <li><a href="/yourbaskets/add?ln=it&recid=2305319">Aggiungi ad un cestino personale</a></li> <li>Esporta come <a style="text-decoration:underline;font-weight:normal" href="/record/2305319/export/hx?ln=it">BibTeX</a>, <a style="text-decoration:underline;font-weight:normal" href="/record/2305319/export/hm?ln=it">MARC</a>, <a style="text-decoration:underline;font-weight:normal" href="/record/2305319/export/xm?ln=it">MARCXML</a>, <a style="text-decoration:underline;font-weight:normal" href="/record/2305319/export/xd?ln=it">DC</a>, <a style="text-decoration:underline;font-weight:normal" href="/record/2305319/export/xe?ln=it">EndNote</a>, <!-- <a style="text-decoration:underline;font-weight:normal" href="/record/2305319/export/xe8x?ln=it">EndNote (8-X)</a>,--> <a style="text-decoration:underline;font-weight:normal" href="/record/2305319/export/xn?ln=it">NLM</a>, <a style="text-decoration:underline;font-weight:normal" href="/record/2305319/export/xw?ln=it">RefWorks</a> </li> </ul> <div style='padding-left: 13px;'> <!-- JQuery Bookmark Button BEGIN --> <div id="bookmark"></div> <div id="bookmark_sciencewise"></div> <style type="text/css"> #bookmark_sciencewise, #bookmark {float: left;} #bookmark_sciencewise li {padding: 2px; width: 25px;} #bookmark_sciencewise ul, #bookmark ul {list-style-image: none;} </style> <script type="text/javascript" src="/js/jquery.bookmark.min.js"></script> <style type="text/css">@import "/css/jquery.bookmark.css";</style> <script type="text/javascript">// <![CDATA[ $.bookmark.addSite('sciencewise', 'ScienceWise.info', 'https://cds.cern.ch/img/sciencewise.png', 'en', 'bookmark', 'http://sciencewise.info/bookmarks/cds:2305319/add'); $('#bookmark_sciencewise').bookmark({sites: ['sciencewise']}); $('#bookmark').bookmark({ sites: ['facebook', 'twitter', 'linkedin', 'google_plusone'], icons: '/img/bookmarks.png', url: 'https://cds.cern.ch/record/2305319', addEmail: true, title: "Applying model checking to critical PLC applications", description: "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." }); // ]]> </script> <!-- JQuery Bookmark Button END --> </div> </div> <div style="clear:both;margin-bottom: 0;"></div> </div> <div class="bottom-left"></div><div class="bottom-right"></div> </div> </div></div> <footer id="footer" class="pagefooter clearfix"> <!-- replaced page footer --> <div class="pagefooterstripeleft"> CERN Document Server :: <a class="footer" href="https://cds.cern.ch/?ln=it">Cerca</a> :: <a class="footer" href="https://cds.cern.ch/submit?ln=it">Sottometti</a> :: <a class="footer" href="https://cds.cern.ch/youraccount/display?ln=it">Personalizza</a> :: <a class="footer" href="https://cds.cern.ch/help/?ln=it">Aiuto</a> :: <a class="footer" href="https://cern.service-now.com/service-portal?id=privacy_policy&se=CDS-Service" target="_blank">Privacy Notice</a> <br /> Fornita da <a class="footer" href="http://invenio-software.org/">Invenio</a> <br /> Mantenuto da <a class="footer" href="https://cern.service-now.com/service-portal?id=service_element&name=CDS-Service">CDS Service</a> - Need help? Contact <a href="https://cern.service-now.com/service-portal?id=service_element&name=CDS-Service">CDS Support</a>. <br /> </div> <div class="pagefooterstriperight"> <div class="cern-logo"> <a id="logo" href="http://cern.ch" title="CERN" rel="CERN" ><img src="https://cds.cern.ch/img/cern_theme/img/cern-logo-large.png" alt="CERN" /></a> </div> <div class="cern-languagebox"> Questo sito è disponibile anche nelle lingue seguenti:<br /><a href="/record/2305319?ln=bg" class="langinfo">Български</a> <a href="/record/2305319?ln=ca" class="langinfo">Català</a> <a href="/record/2305319?ln=de" class="langinfo">Deutsch</a> <a href="/record/2305319?ln=el" class="langinfo">Ελληνικά</a> <a href="/record/2305319?ln=en" class="langinfo">English</a> <a href="/record/2305319?ln=es" class="langinfo">Español</a> <a href="/record/2305319?ln=fr" class="langinfo">Français</a> <a href="/record/2305319?ln=hr" class="langinfo">Hrvatski</a> <span class="langinfo">Italiano</span> <a href="/record/2305319?ln=ja" class="langinfo">日本語</a> <a href="/record/2305319?ln=ka" class="langinfo">ქართული</a> <a href="/record/2305319?ln=no" class="langinfo">Norsk/Bokmål</a> <a href="/record/2305319?ln=pl" class="langinfo">Polski</a> <a href="/record/2305319?ln=pt" class="langinfo">Português</a> <a href="/record/2305319?ln=ru" class="langinfo">Русский</a> <a href="/record/2305319?ln=sk" class="langinfo">Slovensky</a> <a href="/record/2305319?ln=sv" class="langinfo">Svenska</a> <a href="/record/2305319?ln=zh_CN" class="langinfo">中文(简)</a> <a href="/record/2305319?ln=zh_TW" class="langinfo">中文(繁)</a> </div> </div> <!-- replaced page footer --> </footer> <script type="text/javascript"> var SyndeticsBookCovers = (function() { var SMALL_SIZE = "sc.gif", MEDIUM_SIZE = "mc.gif", RAW_URL = "https://secure.syndetics.com/index.aspx?isbn=THEISBN/THESIZE&client=cernlibrary"; replaceCover = function(imgElement, isbns, hdFormat) { var img = new Image(), size = hdFormat ? MEDIUM_SIZE : SMALL_SIZE; var _isbns = isbns.sort(function(a, b) { // sort from shortest to longest ISBN (more modern) return a.length > b.length ? 1 : -1; }); function next() { var isbn = _isbns.pop(); if (isbn) { var url = RAW_URL.replace("THEISBN", isbn).replace("THESIZE", size); img.src = url; } } function done() { imgElement.src = img.src; } img.onload = function() { if (this.width > 1) { done(); } else { next(); } }; next(); }; return { replaceCover: replaceCover }; })(); $(document).ready(function() { // get book covers $("img.book-cover").each(function() { var $this = $(this), strIsbns = $this.data("isbns") || "", isbnsArray = String(strIsbns).split(","), hdFormat = $this.hasClass("hd"); SyndeticsBookCovers.replaceCover(this, isbnsArray, hdFormat); }); // WebNews tooltips $.ajax({ url: "/news/tooltips", success: function(data) { create_tooltips(data); }, dataType: "json", cache: false }); }); </script> <!-- Feedback script --> <script src="//cds.cern.ch/js/feedback.js"></script> <!-- Feedback script --> <!-- Matomo --> <script> var _paq = window._paq = window._paq || []; /* tracker methods like "setCustomDimension" should be called before "trackPageView" */ _paq.push(['trackPageView']); _paq.push(['enableLinkTracking']); (function() { var u="https://webanalytics.web.cern.ch/"; _paq.push(['setTrackerUrl', u+'matomo.php']); _paq.push(['setSiteId', '756']); var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0]; g.async=true; g.src=u+'matomo.js'; s.parentNode.insertBefore(g,s); })(); </script> <!-- End Matomo Code --> </body> </html>