Systematic derivation of a validation model from a rule-oriented model: a system validation case study using PROMELA/SPIN

We propose an approach to validate a logical rule-oriented model by a systematic derivation of the associated PROMELA validation model. The derivation is done on the basis of a control-oriented system architecture which is carefully built. The obtained model is increased with correctness properties (safety and liveness properties) and is then validated using the SPIN tool. SPIN is a model checker and more generally a verification tool that supports the design and verification of asynchronous processes. PROMELA is the input language of SPIN. A PROMELA model is a CSP-like description of communicating asynchronous processes. The interest of our approach is that an initial logical model can be systematically reused for the validation instead of specifying a particular state machine model. This work presents the approach and its application to an industrial case study about a nuclear power station cooling system.