guest ::
| Home > Publications database > Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study > print |
| 001 | 364952 | ||
| 005 | 20260120231511.0 | ||
| 020 | _ | _ | |a 978-3-031-93705-7 (print) |
| 020 | _ | _ | |a 978-3-031-93706-4 (electronic) |
| 024 | 7 | _ | |a 10.1007/978-3-031-93706-4_13 |2 doi |
| 024 | 7 | _ | |a 0302-9743 |2 ISSN |
| 024 | 7 | _ | |a 1611-3349 |2 ISSN |
| 037 | _ | _ | |a GSI-2026-00321 |
| 100 | 1 | _ | |a Dutle, Aaron |0 0000-0002-8503-5514 |b 0 |e Editor |
| 111 | 2 | _ | |a 17th International Symposium on NASA Formal Methods-NFM, VA |c Virgina |d 2025-06-11 - 2025-06-13 |w usa |
| 245 | _ | _ | |a Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study |
| 260 | _ | _ | |a Cham |c 2025 |b Springer Nature Switzerland |
| 295 | 1 | 0 | |a NASA 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 |
| 300 | _ | _ | |a 227 - 235 |
| 336 | 7 | _ | |a CONFERENCE_PAPER |2 ORCID |
| 336 | 7 | _ | |a Conference Paper |0 33 |2 EndNote |
| 336 | 7 | _ | |a INPROCEEDINGS |2 BibTeX |
| 336 | 7 | _ | |a conferenceObject |2 DRIVER |
| 336 | 7 | _ | |a Output Types/Conference Paper |2 DataCite |
| 336 | 7 | _ | |a Contribution to a conference proceedings |b contrib |m contrib |0 PUB:(DE-HGF)8 |s 1768929498_3310668 |2 PUB:(DE-HGF) |
| 336 | 7 | _ | |a Contribution to a book |0 PUB:(DE-HGF)7 |2 PUB:(DE-HGF) |m contb |
| 490 | 0 | _ | |a Lecture Notes in Computer Science |v 15682 |
| 520 | _ | _ | |a The 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. |
| 536 | _ | _ | |a 6G14 - GSI-MU Ion Facilities (POF4-6G14) |0 G:(DE-HGF)POF4-6G14 |c POF4-6G14 |f POF IV |x 0 |
| 588 | _ | _ | |a Dataset connected to DataCite |
| 693 | _ | _ | |1 EXP:(DE-Ds200)Altdaten-20200803 |0 EXP:(DE-Ds200)Altdaten-20200803 |a Facility Altdaten therefore no facility |x 0 |
| 700 | 1 | _ | |a Humphrey, Laura |0 0000-0002-3148-9035 |b 1 |e Editor |
| 700 | 1 | _ | |a Titolo, Laura |0 0000-0001-7820-7640 |b 2 |e Editor |
| 700 | 1 | _ | |a Lopez-Miguel, Ignacio D. |0 0000-0002-8044-0385 |b 3 |
| 700 | 1 | _ | |a Adiego, Borja Fernández |b 4 |
| 700 | 1 | _ | |a Salinas, Matias |0 P:(DE-HGF)0 |b 5 |
| 700 | 1 | _ | |a Betz, Christine |0 P:(DE-Ds200)OR3416 |b 6 |u gsi |
| 773 | _ | _ | |a 10.1007/978-3-031-93706-4_13 |
| 909 | C | O | |o oai:repository.gsi.de:364952 |p VDB |
| 910 | 1 | _ | |a GSI Helmholtzzentrum für Schwerionenforschung GmbH |0 I:(DE-Ds200)20121206GSI |k GSI |b 5 |6 P:(DE-HGF)0 |
| 910 | 1 | _ | |a GSI Helmholtzzentrum für Schwerionenforschung GmbH |0 I:(DE-Ds200)20121206GSI |k GSI |b 6 |6 P:(DE-Ds200)OR3416 |
| 913 | 1 | _ | |a DE-HGF |b Forschungsbereich Materie |l Großgeräte: Materie |1 G:(DE-HGF)POF4-6G0 |0 G:(DE-HGF)POF4-6G14 |3 G:(DE-HGF)POF4 |2 G:(DE-HGF)POF4-600 |4 G:(DE-HGF)POF |v GSI-MU Ion Facilities |x 0 |
| 915 | _ | _ | |a Nationallizenz |0 StatID:(DE-HGF)0420 |2 StatID |d 2024-12-28 |w ger |
| 915 | _ | _ | |a DBCoverage |0 StatID:(DE-HGF)0200 |2 StatID |b SCOPUS |d 2024-12-28 |
| 920 | 1 | _ | |0 I:(DE-Ds200)ACO-20051214OR053 |k ACO |l Accelerator Controls |x 0 |
| 980 | _ | _ | |a contrib |
| 980 | _ | _ | |a VDB |
| 980 | _ | _ | |a contb |
| 980 | _ | _ | |a I:(DE-Ds200)ACO-20051214OR053 |
| 980 | _ | _ | |a UNRESTRICTED |
| Library | Collection | CLSMajor | CLSMinor | Language | Author |
|---|