TY - GEN
T1 - VIS Analyzer
T2 - 13th IEEE International Symposium on Object, Component, and Service-Oriented Real-Time Distributed Computing, ISORC 2010
AU - Jeong, Sehun
AU - Yoo, Junbeom
AU - Cha, Sungdeok
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=77954763818&partnerID=8YFLogxK
U2 - 10.1109/ISORC.2010.41
DO - 10.1109/ISORC.2010.41
M3 - Conference contribution
AN - SCOPUS:77954763818
SN - 9780769540375
T3 - ISORC 2010 - 2010 13th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing
SP - 250
EP - 254
BT - ISORC 2010 - 2010 13th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing
Y2 - 5 May 2010 through 6 May 2010
ER -