Formal Probabilistic Risk Assessment of a Nuclear Power Plant
summary
Formalizes a Boiling Water Reactor as a BWR functional block diagram in the HOL4 theorem prover, proves explicit event-class theorems (containment intact/fails under melt and pressure scenarios), and computes exact probabilities for four accident classes. Results match a specialized Isograph/analytical baseline, outperform MATLAB (example 0.019 vs 0.013 for one class) and show CPU time improvement and better scalability. Implementation handles multi-state components; future work targets dynamic failures with conditional probabilities.
AI-written summary · about
chapters (12)
- 0:00Formal probabilistic risk assessment intro
- 1:25Motivation for safety-critical PRA
- 3:52Reliability modeling methods
- 6:22Functional block diagrams steam turbine
- 9:14Probability calculations in reliability
- 12:05Formal methods for PRA
- 13:26Nuclear plant structure safety
- 15:39Accident modeling with block diagrams
- 17:30Hierarchical modeling in FBDs
- 19:18Proving containment failure theorems
- 20:44Experimental comparison tools
- 23:12Conclusion future work