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

    5 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
    Country/TerritorySpain
    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