VIS Analyzer: A Visual Assistant for VIS Verification and Analysis

Formal verification plays an important role in demonstrating the quality of safety-critical systems such as nuclear power plants. We have used the VIS verification system to determine behavioral equivalence between two successive revisions in developing the KNICS RPS (Reactor Protection System) in Korea. The VIS accepts a high-level programming language Verilog 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 to demonstrate its effectiveness and usefulness.