VIS Analyzer: A visual assistant for VIS verification and analysis

Sehun Jeong, Junbeom Yoo, Sungdeok Cha

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

Formal verification plays an important role in demonstrating the quality of safety-critical [1] systems such as nuclear power plants. We have used the VIS verification system [2] to determine behavioral equivalence between two successive revisions in developing the KNICS RPS (Reactor Protection System) [3] in Korea. The VIS accepts a high-level programming language Verilog [4] as input, and its verification results contain valuable information about one reason of the failure. However the VIS offers no graphical interface, and partially displays relevant information necessary to understand the full verification scenario accurately. Many nuclear engineers and verification experts found the information insufficient, and it makes hard to the wide use of the VIS verification system in industry. This paper proposes the VIS Analyzer, a visual assistant for VIS verification and analysis, which can help nuclear engineers take full benefits of VIS without being overwhelmed by incomplete and low-level details. The VIS Analyzer automates the VIS verification processes such as equivalence checking and model checking, and displays the verification results in visual formats. We used a recent case study introduced in [5] to demonstrate its effectiveness and usefulness.

Original languageEnglish
Title of host publicationISORC 2010 - 2010 13th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing
Pages250-254
Number of pages5
DOIs
Publication statusPublished - 2010
Event13th IEEE International Symposium on Object, Component, and Service-Oriented Real-Time Distributed Computing, ISORC 2010 - Carmona, Sevilla, Spain
Duration: 2010 May 52010 May 6

Publication series

NameISORC 2010 - 2010 13th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing
Volume1

Other

Other13th IEEE International Symposium on Object, Component, and Service-Oriented Real-Time Distributed Computing, ISORC 2010
CountrySpain
CityCarmona, Sevilla
Period10/5/510/5/6

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Computer Science Applications
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'VIS Analyzer: A visual assistant for VIS verification and analysis'. Together they form a unique fingerprint.

  • Cite this

    Jeong, S., Yoo, J., & Cha, S. (2010). VIS Analyzer: A visual assistant for VIS verification and analysis. In ISORC 2010 - 2010 13th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (pp. 250-254). [5479548] (ISORC 2010 - 2010 13th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing; Vol. 1). https://doi.org/10.1109/ISORC.2010.41