Formal Method in Fault Tolerant Software Architecture Domain

• GFTSA applied to the safety critical system LDAS

                1. The formal model of GFTSA is presented  here.

                2. The x-frames built for the template of GFTSA in XVCL are all presented here.

                3. The x-frames built for LDAS in XVCL are all presented here.

                4. The formal model of LDAS is presented here.

• FTA applied to the mission critical system SCS

          1. The formal model of FTA  is presented here.

               2.  The formal proof of FTA is presented here.

          3. The x-frames built for the template of FTA and the semantic rules are presented here.

               4. The x-frames built for SCS and the formal model of SCS are presented here.

               5. The formal proof of SCS is presented here.

•  The Mechanical Verification of GFTSA in PVS

         1. The PVS model of GFTSA  is presented here.

         2.  The proof scripts for the fault tolerant properties of  GFTSA is presented here.

              3. The x-frames built for the template of PVS specification and proof scripts are presented here.

         4. The PVS specification and proof scripts of EPS are presented here.

   Publication:

              1. Mechanical Verification of Fault Tolerant Architecture in a Prototype Verification System.

              2. Generic Fault Tolerant Software Architecture Reasoning and Customization.

              3. Modeling and Customization of Fault Tolerant Architecture Using Object-Z/XVCL.