Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Synthesis-Aided Reliability Assurance of Basic Block Models for Model Checking Purposes
Aalto University, Department of Electrical Engineering and Automation, Espoo, Finland; Computer Technology Department, ITMO University, St. Petersburg, Russian Federation.
VTT Technical Research Centre of Finland Ltd., Espoo, Finland.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science. Aalto University, Department of Electrical Engineering and Automation, Espoo, Finland.ORCID iD: 0000-0002-9315-9920
2018 (English)In: Proceedings of the 2018 IEEE 27th International Symposium on Industrial Electronics (ISIE), IEEE, 2018, p. 669-674, article id 8433793Conference paper, Published paper (Refereed)
Abstract [en]

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. 

Place, publisher, year, edition, pages
IEEE, 2018. p. 669-674, article id 8433793
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-70797DOI: 10.1109/ISIE.2018.8433793Scopus ID: 2-s2.0-85052369562ISBN: 9781538637050 (print)ISBN: 978-1-5386-3705-0 (electronic)ISBN: 978-1-5386-3704-3 (print)OAI: oai:DiVA.org:ltu-70797DiVA, id: diva2:1246437
Conference
IEEE 27th International Symposium on Industrial Electronics, ISIE 2018; Cairns; Australia; 13-15 June 2018
Available from: 2018-09-07 Created: 2018-09-07 Last updated: 2018-09-07Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Vyatkin, Valeriy

Search in DiVA

By author/editor
Vyatkin, Valeriy
By organisation
Computer Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 3 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf