% IMPORTANT: The following is UTF-8 encoded.  This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.

@INPROCEEDINGS{Dutle:364952,
      author       = {Lopez-Miguel, Ignacio D. and Adiego, Borja Fernández and
                      Salinas, Matias and Betz, Christine},
      editor       = {Dutle, Aaron and Humphrey, Laura and Titolo, Laura},
      title        = {{F}ormal {V}erification of {PLC}s as a {S}ervice: {A}
                      {CERN}-{GSI} {S}afety-{C}ritical {C}ase {S}tudy},
      volume       = {15682},
      address      = {Cham},
      publisher    = {Springer Nature Switzerland},
      reportid     = {GSI-2026-00321},
      isbn         = {978-3-031-93705-7 (print)},
      series       = {Lecture Notes in Computer Science},
      pages        = {227 - 235},
      year         = {2025},
      comment      = {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},
      booktitle     = {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},
      abstract     = {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.},
      month         = {Jun},
      date          = {2025-06-11},
      organization  = {17th International Symposium on NASA
                       Formal Methods-NFM, VA, Virgina (usa),
                       11 Jun 2025 - 13 Jun 2025},
      cin          = {ACO},
      cid          = {I:(DE-Ds200)ACO-20051214OR053},
      pnm          = {6G14 - GSI-MU Ion Facilities (POF4-6G14)},
      pid          = {G:(DE-HGF)POF4-6G14},
      experiment   = {EXP:(DE-Ds200)Altdaten-20200803},
      typ          = {PUB:(DE-HGF)8 / PUB:(DE-HGF)7},
      doi          = {10.1007/978-3-031-93706-4_13},
      url          = {https://repository.gsi.de/record/364952},
}