Formal Modeling and Quantitative Evaluation for Online Monitoring Systems in Nuclear Facilities

Advanced online execution monitoring is an essential system for ensuring the safety of nuclear facilities. Formal modeling and quantitative evaluation of these systems offer a promising approach to verifying their behaviors and identifying potential vulnerabilities. However, existing modeling languages often lack the capability to represent the system's control flow logic. Additionally, the absence of automated transformation rules hinders the verification of generated models using available verification tools. Hence, in this paper, we propose a novel synchronous modeling language, Hybrid SynLong, which integrates data flow and control flow to effectively describe the real-time dynamic behaviors of online monitoring systems. Additionally, we present a method for converting the Hybrid SynLong language model into a network of stochastic hybrid automata, enabling direct verification with existing statistical model checkers. In consequence, the performance of an online monitoring system can be quantitatively evaluated by executing well-defined queries. The experimental results illustrate the effectiveness and efficiency of the proposed modeling language and transformation algorithms, as demonstrated through their application in an online monitoring system for a nuclear plant.