[FTSCS] Formal Probabilistic Risk Assessment of a Nuclear Power Plant
Functional Block Diagrams (FBD) are commonly used as a graphical representation for probabilistic risk assessment in a wide range of complex engineering applications. An FBD models the stochastic behavior and cascading dependencies of system components or subsystems. Within FBD-based safety analysis, Event Trees (ET) dependability modeling techniques are typically used to associate all possible risk events to each subsystem. In this paper, we conduct the formal modeling and probabilistic risk assessment of a nuclear power plant in the HOL4 theorem prover. Using an FBD modeling in HOL4 of the nuclear Boiling Water Reactor (BWR), we formally determine all possible classes of accident events that can occur in the BWR. We compare our formal analysis in HOL4 with those obtained analytically and by simulation using Matlab and the specialized Isograph tool. Experimental results showed the superiority of our approach in terms of scalability, expressiveness, accuracy and CPU time.
Видео [FTSCS] Formal Probabilistic Risk Assessment of a Nuclear Power Plant канала ACM SIGPLAN
Видео [FTSCS] Formal Probabilistic Risk Assessment of a Nuclear Power Plant канала ACM SIGPLAN
Показать
Комментарии отсутствуют
Информация о видео
Другие видео канала
TyDe 2021 - Interactive Haskell Type Inference Exploration (Extended Abstract)[OCaml'22] Efficient “out of heap” pointers for multicore OCaml[PriSC'22] Composing Secure CompilersWarping Cache Simulation of Polyhedral Programs[SLE] Property-Based Testing: Climbing the Stairway to Verification[ML'22] Efficient and Scalable Parallel Functional Programming Through Disentanglement[CPP'23] CompCert: a journey through the landscape of mechanized semantics for verified co...Low-Latency, High-Throughput Garbage CollectionDISTAL: The Distributed Tensor Algebra CompilerIRDL: An IR Definition Language for SSA CompilersEfficient Compilation of Algebraic Effect Handlers[ICFP'22] Safe Couplings: Coupled Refinement TypesWebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration[ICFP'22] Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structu…Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation LogicInterval Universal Approximation for Neural Networks (Teaser)[POPL'22] Layered and Object-Based Game Semantics[POPL'22] Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites[VMCAI'22] Making PROGRESS in Property Directed ReachabilityPrinciples and Patterns of JastAdd-Style Reference Attribute GrammarsNatural Language-Guided Programming