Verification of fault tolerant safety I&C systems using model checking

Antti Pakonen, Igor Buzhinsky

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

2 Sitaatiot (Scopus)

Abstrakti

Model checking has been successfully used for detailed formal verification of instrumentation and control (I&C) systems, as long as the focus has been on the application logic, alone. In safety-critical applications, fault tolerance is also an important aspect, but introducing I&C hardware failure modes to the formal models comes at a significant computational cost. Previous attempts have led to state space explosion, and prohibitively long processing times. In this paper, we present a method for adding hardware component failures and communication delays into I&C application logic models for the NuSMV symbolic model checker. Based on a case study built around a semi-fictitious, four-redundant nuclear power plant protection system, we demonstrate how even detailed system designs can be verified, if the focus is kept on single failure tolerance.

AlkuperäiskieliEnglanti
OtsikkoProceedings of the 20th IEEE International Conference on Industrial Technology, ICIT 2019
KustantajaIEEE
Sivut969-974
Sivumäärä6
ISBN (elektroninen)9781538663769
DOI - pysyväislinkit
TilaJulkaistu - 1 helmikuuta 2019
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaIEEE International Conference on Industrial Technology - Melbourne, Austraalia
Kesto: 13 helmikuuta 201915 helmikuuta 2019

Julkaisusarja

NimiProceedings of the IEEE International Conference on Industrial Technology
Vuosikerta2019-February
ISSN (painettu)2641-0184
ISSN (elektroninen)2643-2978

Conference

ConferenceIEEE International Conference on Industrial Technology
LyhennettäICIT
MaaAustraalia
KaupunkiMelbourne
Ajanjakso13/02/201915/02/2019

Sormenjälki

Sukella tutkimusaiheisiin 'Verification of fault tolerant safety I&C systems using model checking'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä