English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Dynamic reliability block diagrams (DRBDs) are introduced to overcome themodeling limitations of traditional reliability block diagrams, such as theinability to capture redundant components. However, so far there is noalgebraic framework that allows conducting the analysis of a given DRBD basedon its structure function and enables verifying its soundness usinghigher-order logic (HOL) theorem proving. In this work, we propose a newalgebra to formally express the structure function and the reliability of aDRBD with spare constructs based on basic system blocks and newly introducedDRBD operators. We present several simplification properties that allowreducing the structure of a given DRBD. We provide the HOL formalization of theproposed algebra, and formally verify its corresponding properties using theHOL4 theorem prover. This includes formally verifying generic reliabilityexpressions of the spare construct, series, parallel and deeper structures inan extensible manner that allows verifying the reliability of complex systems.Finally, we demonstrate the applicability of this algebra by formally analyzingthe terminal reliability analysis of a shuffle-exchange network in HOL4.

A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams