Stochastic Zélus: Stochastic Hybrid Modeling and Verification for Nuclear I&C System

  • Jiang Xiong*
  • , Letian Fang
  • , Jing Liu
  • , Mingxing Liu
  • *Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

The Zélus language excels at describing hybrid systems but has limitations in handling uncertainties, such as probabilistic transitions and random failures, in nuclear Instrumentation and Control (I&C) systems. Other languages for modeling uncertainty often choose to discretize the continuous behavior in the system, making it difficult to accurately describe the system. To address this, we propose Stochastic Zélus, a new language integrating probabilistic automata for modeling hybrid systems in uncertain environments. We also developed a quantitative analysis framework and a prototype tool for converting Stochastic Zélus models to NSHA (Networks of Stochastic Hybrid Automata) models supported by UPPAAL-SMC, to support quantitative analysis of stochastic Zélus models using UPPAAL-SMC. Finally, we demonstrate the effectiveness of this approach through a case study on a Reactor Protection System (PS), proving that the method is effective in verifying the reliability of the PS in uncertain environments.

Original languageEnglish
Title of host publicationProceedings - SEKE 2025
Subtitle of host publication37th International Conference on Software Engineering and Knowledge Engineering
PublisherKnowledge Systems Institute Graduate School
Pages366-371
Number of pages6
ISBN (Electronic)1891706624
DOIs
StatePublished - 2025
Event37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025 - Hybrid, Pompeii, Italy
Duration: 29 Sep 20254 Oct 2025

Publication series

NameProceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
ISSN (Print)2325-9000
ISSN (Electronic)2325-9086

Conference

Conference37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025
Country/TerritoryItaly
CityHybrid, Pompeii
Period29/09/254/10/25

Keywords

  • Formal Method
  • Nuclear I&C System
  • Stochastic Zélus
  • UPPAAL-SMC

Fingerprint

Dive into the research topics of 'Stochastic Zélus: Stochastic Hybrid Modeling and Verification for Nuclear I&C System'. Together they form a unique fingerprint.

Cite this