Implementation Of An Industrial Safety Protocol Model By Using TLA

As increasing safety-critical systems are used in our daily life, safety engineering attracts more attentions. Under this circumstance, the international functional safety standard IEC 61508 was developed. It describes system safety by the term Safety Integrity Levels (SIL), and recommends many formal methods to verify system safety. Formal methods basically verify three major properties of the system: safeness, liveness and fairness. However, we also discussed three main problems of formal methods. The most important one is the state explosion.In this thesis, we introduced TLA and some prerequisite mathematical knowledge. Then we proposed a divide and conquer paradigm for specification refinement to reduce system complexity. The basic principle is to simplify the system specification from an easy conceptual model. Then we decomposed the system into sub-modules and add system behaviors and data exchanges to them. Meanwhile we analyzed what system features can be omitted, which won't break system integrity. After that we integrated these sub-modules to a whole one and analyzed the three major properties mentioned above. We also proposed a modeling mechanism called Module State Machine, which is able to be interpreted to TLA model easily.At last, we discussed the experiment result of the TLA model checking. The conclusion is that the system satisfies safeness property, but as the limitations of TLA and its model checker TLC, liveness and fairness properties cannot be checked at the moment. We analyzed the reason of this result and also forecasted the future research approach of formal verification in industry.