(******************************************************************) (* DRBD algebraic analysis IN HOL4 *) (* *) (* Copyright 2019, Yassmeen Elderhalli *) (* *) (* Contact: y_elderh@encs.concordia.ca *) (* *) (******************************************************************) INSTALLATION: Requirement: HOL4 "Kananaskis" 12 release, polyml 5.7 1) Download "Required-Theories.zip" This archive contains some required theories including - The extreal, measure and probability theories developed by Tarek Mhamdi for extended real datatypes - The lebesgue measure theory and some other theories ported (from HOL light and Isablle/HOL) by Mohamed Qasim - The PIE_EXTREAL theory developed by Waqar Ahmad 2) Download "DFT-Thoeries.zip" This archive contains: - integration_before_afterScript.sml which has the Pr (X < Y /\ Y <=t) and Pr (X < Y /\ X <=t) - DFT_Gates_def_PROBScript.sml which has the definitions of the gates, their probabilities and the simplification theorems - WCSPScript.sml which has the probabilistic behavior for the Warm and Cold spare gates. - Holmakefile which is required to include the path for the "Required-Theories" directory, the path in the file should be changed to point to the path of the "Required-Theories" directory 3) Download "DRBD-Thoeries.zip" This archive contains: - The "DRBDScript.sml" which has DRBD operators and constructs definitions and verified reliability expressions - The "SENplusScript.sml" which has the verified terminal reliability of the shuffle-exchange network - The "DBWScript.sml" which has the verified reliability of the drive-by-wire system - Holmakefile which is required to include the path for the "Required-Theories" and "DFT-Theories" directories, the path in the file should be changed to point to the path of these directories. 3) run Holmake to build the theories in the Required-Theories, DFT-Theories directories and DRBD theories 4) Below are the names of the definitions and theorems that correspond to the definitions and theorems in the paper: (*************************************************************************) (* Section 3.2 DRBD Event *) (*************************************************************************) Definition 3: DRBD_event_def Definition 4: Rel_def Theorem 1: CDF_Rel (*************************************************************************) (* Section 3.3 Identity elements, operators and simplification theorems *) (*************************************************************************) Table 5: --------- Always element: R_ALWAYS_def Never element: R_NEVER_def AND operator: R_AND_def OR operator: R_OR_def After operator: R_AFTER_def Simultaneous operator: R_SIMULT_def Inclusive After operator: R_INCLUSIVE_AFTER_def --------- Theorem 2: Rel_R_AND Theorem 3: Rel_R_OR Definition 5: nR_AND_def Definition 6: nR_OR_def Theorem 4: Rel_R_AFTER (*************************************************************************) (* Section 3.4 DRBD Constructs and theire reliability Expressions *) (*************************************************************************) Definition 7 (Warm Spare Construct): R_WSP_def Definition of Hot Spare Construct (not in paper): R_HSP_def Definition of Cold Spare Construct (not in paper): R_CSP_def Theorem 5 (Reliability of WSP): Rel_R_WSP Theorem of reliability of HSP (not in paper) : Rel_R_HSP Theorem of reliability of CSP (not in paper) : Rel_R_CSP Table 6: --------- Definition DRBD series structure: DRBD_series_def Definition DRBD parallel sructure: DRBD_parallel_def Theorem of reliability of series structure: PROB_DRBD_series_rv Theorem of reliability of parallel structure: PROB_DRBD_parallel_rv --------- Definition 8: rv_to_event_def Theorem 6: nR_AND_DRBD_series Theorem 7: nR_OR_DRBD_parallel Table 7: --------- Theorem of reliability of series-parallel structure: PROB_DRBD_series_parallel_rv_red Theorem of reliability of parallel-series structure: PROB_DRBD_parallel_series_rv_red --------- Theorem 8: indep_sets_collect_sigma_BIGUNION_events independence of intersection of partitions (in technical report): indep_sets_collect_sigma_BIGINTER_events reliability of 4-level series-parallel-series-parallel structure (in technical report): PROB_DRBD_nested_series_parallel_rv_red (*************************************************************************) (* Section 4 Applications *) (*************************************************************************) expressing the SEN using the operators (in technical report): SEN_nR_AND Theorem 9: Rel_DRBD_SEN_plus Theorem of reliability of SENplus with the expression of the WSP (not in paper): Rel_DRBD_SEN_plus1 Theorem of reliability of DBW (in technical report): Rel_DBW (*************************************************************************) (* Section 3.1 HOL probability theory (preliminaries) *) (*************************************************************************) Definition 1: random_variable_def Definition 2: CDF_def