Dynamic Fault Trees (DFTs) model the failure behavior of systems dynamics. Several rewriting rules have been recently developed, which allow the simplification of DFTs prior to a formal analysis with tools such as the Storm model checker. To ascertain the soundness of the analysis, we propose to formally verify these rewriting rules using higher-order-logic (HOL) theorem proving. We first present the formalization in HOL of commonly used DFT gates, i.e., AND, OR and PAND, with an arbitrary number of inputs. Then we describe our formal specification of the rewriting rules and the verification of their intended behavior using the HOL4 theorem prover.
CITATION STYLE
Elderhalli, Y., Volk, M., Hasan, O., Katoen, J. P., & Tahar, S. (2019). Formal Verification of Rewriting Rules for Dynamic Fault Trees. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11724 LNCS, pp. 513–531). Springer Verlag. https://doi.org/10.1007/978-3-030-30446-1_27
Mendeley helps you to discover research relevant for your work.