000364952 001__ 364952
000364952 005__ 20260120231511.0
000364952 020__ $$a978-3-031-93705-7 (print)
000364952 020__ $$a978-3-031-93706-4 (electronic)
000364952 0247_ $$2doi$$a10.1007/978-3-031-93706-4_13
000364952 0247_ $$2ISSN$$a0302-9743
000364952 0247_ $$2ISSN$$a1611-3349
000364952 037__ $$aGSI-2026-00321
000364952 1001_ $$00000-0002-8503-5514$$aDutle, Aaron$$b0$$eEditor
000364952 1112_ $$a17th International Symposium on NASA Formal Methods-NFM, VA$$cVirgina$$d2025-06-11 - 2025-06-13$$wusa
000364952 245__ $$aFormal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study
000364952 260__ $$aCham$$bSpringer Nature Switzerland$$c2025
000364952 29510 $$aNASA Formal Methods / Dutle, Aaron (Editor) [https://orcid.org/0000-0002-8503-5514] ; Cham : Springer Nature Switzerland, 2025, Chapter 13 ; ISSN: 0302-9743=1611-3349 ; ISBN: 978-3-031-93705-7=978-3-031-93706-4 ; doi:10.1007/978-3-031-93706-4
000364952 300__ $$a227 - 235
000364952 3367_ $$2ORCID$$aCONFERENCE_PAPER
000364952 3367_ $$033$$2EndNote$$aConference Paper
000364952 3367_ $$2BibTeX$$aINPROCEEDINGS
000364952 3367_ $$2DRIVER$$aconferenceObject
000364952 3367_ $$2DataCite$$aOutput Types/Conference Paper
000364952 3367_ $$0PUB:(DE-HGF)8$$2PUB:(DE-HGF)$$aContribution to a conference proceedings$$bcontrib$$mcontrib$$s1768929498_3310668
000364952 3367_ $$0PUB:(DE-HGF)7$$2PUB:(DE-HGF)$$aContribution to a book$$mcontb
000364952 4900_ $$aLecture Notes in Computer Science$$v15682
000364952 520__ $$aThe increased technological complexity and demand for software   reliability require organizations to formally design and verify their   safety-critical programs to minimize systematic failures. Formal methods   are recommended by functional safety standards (e.g., by IEC 61511 for   the process industry and by the generic IEC 61508) and play a crucial   role. Their structured approach reduces ambiguity in system   requirements, facilitating early error detection. This paper introduces   a formal verification service for PLC (programmable logic controller)   programs compliant with functional safety standards, providing external   expertise to organizations while eliminating the need for extensive   internal training. It offers a cost-effective solution to meet the   rising demands for formal verification processes. The approach is   extended to include modeling time-dependent, know-how-protected   components, enabling formal verification of real safety-critical   applications. A case study shows the application of PLC formal   verification as a service provided by CERN in a safety-critical   installation at the GSI particle accelerator facility.
000364952 536__ $$0G:(DE-HGF)POF4-6G14$$a6G14 - GSI-MU Ion Facilities (POF4-6G14)$$cPOF4-6G14$$fPOF IV$$x0
000364952 588__ $$aDataset connected to DataCite
000364952 693__ $$0EXP:(DE-Ds200)Altdaten-20200803$$1EXP:(DE-Ds200)Altdaten-20200803$$aFacility Altdaten therefore no facility$$x0
000364952 7001_ $$00000-0002-3148-9035$$aHumphrey, Laura$$b1$$eEditor
000364952 7001_ $$00000-0001-7820-7640$$aTitolo, Laura$$b2$$eEditor
000364952 7001_ $$00000-0002-8044-0385$$aLopez-Miguel, Ignacio D.$$b3
000364952 7001_ $$aAdiego, Borja Fernández$$b4
000364952 7001_ $$0P:(DE-HGF)0$$aSalinas, Matias$$b5
000364952 7001_ $$0P:(DE-Ds200)OR3416$$aBetz, Christine$$b6$$ugsi
000364952 773__ $$a10.1007/978-3-031-93706-4_13
000364952 909CO $$ooai:repository.gsi.de:364952$$pVDB
000364952 9101_ $$0I:(DE-Ds200)20121206GSI$$6P:(DE-HGF)0$$aGSI Helmholtzzentrum für Schwerionenforschung GmbH$$b5$$kGSI
000364952 9101_ $$0I:(DE-Ds200)20121206GSI$$6P:(DE-Ds200)OR3416$$aGSI Helmholtzzentrum für Schwerionenforschung GmbH$$b6$$kGSI
000364952 9131_ $$0G:(DE-HGF)POF4-6G14$$1G:(DE-HGF)POF4-6G0$$2G:(DE-HGF)POF4-600$$3G:(DE-HGF)POF4$$4G:(DE-HGF)POF$$aDE-HGF$$bForschungsbereich Materie$$lGroßgeräte: Materie$$vGSI-MU Ion Facilities$$x0
000364952 915__ $$0StatID:(DE-HGF)0420$$2StatID$$aNationallizenz$$d2024-12-28$$wger
000364952 915__ $$0StatID:(DE-HGF)0200$$2StatID$$aDBCoverage$$bSCOPUS$$d2024-12-28
000364952 9201_ $$0I:(DE-Ds200)ACO-20051214OR053$$kACO$$lAccelerator Controls$$x0
000364952 980__ $$acontrib
000364952 980__ $$aVDB
000364952 980__ $$acontb
000364952 980__ $$aI:(DE-Ds200)ACO-20051214OR053
000364952 980__ $$aUNRESTRICTED