Synthesis-Aided Reliability Assurance of Basic Block Models for Model Checking Purposes

Igor Buzhinsky, Antti Pakonen, Valeriy Vyatkin

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

2 Sitaatiot (Scopus)
136 Lataukset (Pure)

Abstrakti

In the Finnish nuclear industry, model checking, a formal verification technique, is used as an additional means of safety assurance for instrumentation and control (IC) system design. Since the code of vendor-specific basic function blocks used in IC is commonly closed, these blocks need to be modeled manually based on available specification. This modeling introduces an additional source of human factor into the verification process. To increase the reliability of the library of basic blocks used in nuclear IC verification, we apply formal synthesis techniques, which can construct finite-state models of reactive systems from behavior examples and temporal properties. Since these techniques have computational limitations and synthesized models are hard to understand even by an analyst, we do not use them in the final verification process. Instead, in an iterative process, behavioral differences between a synthesized model and a manual model implementation are identified and used to create a list of features of manual implementations which either violate the specification or show that the specification is ambiguous.

AlkuperäiskieliEnglanti
OtsikkoProceedings of the 2018 IEEE 27th International Symposium on Industrial Electronics, ISIE 2018
KustantajaIEEE
Sivut669-674
Sivumäärä6
Vuosikerta2018-June
ISBN (painettu)9781538637050
DOI - pysyväislinkit
TilaJulkaistu - 10 elokuuta 2018
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Symposium on Industrial Electronics - Cairns, Austraalia
Kesto: 13 kesäkuuta 201815 kesäkuuta 2018
Konferenssinumero: 27

Julkaisusarja

NimiProceedings of the IEEE International Symposium on Industrial Electronics
KustantajaIEEE
ISSN (painettu)2163-5137
ISSN (elektroninen)2380-1395

Conference

ConferenceInternational Symposium on Industrial Electronics
LyhennettäISIE
MaaAustraalia
KaupunkiCairns
Ajanjakso13/06/201815/06/2018

Sormenjälki

Sukella tutkimusaiheisiin 'Synthesis-Aided Reliability Assurance of Basic Block Models for Model Checking Purposes'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä