Chanjuan Li, Nicholas Mc Guire, Qingguo Zhou, School of Information Science and Engineering, Lanzhou University, China

Formal verification play an important role in development and application of safety-critical system, which is highly recommended at SIL4 in IEC61508.  SPIN as a powerful model checker verifies the correctness of distributed software models in a rigorous and mostly automated fashion. Promela(Process Meta Language)supports modeling of asynchronous distributed algorithms as non-deterministic automata, data structures allowing detail where appropriate and Linear temporal logic expressing verified safety and liveness properties.

The object to be verified is the protocol - NOP designed for safety-critical distributed embedded system, which provides comparative connectivity semantic to time-triggered protocol through deciding the ordering of access to shared medium by a pre-defined node order. However, NOP use an event-trigger paradigm instead of time-triggered, thus communication events including error detection is based on discrete events instead of real time, which make it possible to use SPIN as validation tool.

The objective of this paper is to verify the design of NOP showing that it meets the fault tolerant requirement. According to the fault hypothesis, NOP has performance failure semantic that is a faulty node deliver correct results in the value domain,but in time domain, the results may be delivered early or late. Therefore modeling the protocol with all faults and reaction in one model would generate huge state space which consumes much more computation time and resources. NOP assumes that only one fault occurs at any time, and that a subsequent fault will occur no earlier than the response completion time for the first fault. Thus, to reduce state space, we partition the model by separating out the classes of fault that can occur into dedicated models. Each can be treated independently of the others, significantly reducing the size of the overall state space to be checked by the validation process and making the model more understandable. Finally, based on properties verified by each model, the safety and liveness properties of NOP can be validated by integrating the results of each model because the full coverage of faults and independence of models.In this paper, we  partition the protocol model into four equivalence classes.  The detail of each model are described, and the validation results is analyzed. Based on this work, at the end of paper, we prove the correctness of design of NOP meeting the fault tolerant requirement by composing the verified properties. At the same time, we show that the feedback of the validation process facilitates improvement of the protocol design.