A Mechanized Formal Refinement Proof of Modbus Communication Using Event-B Proof System
Sanae El Mimouni, Mohamed Bouhdadi · International journal of intelligent engineering and systems · 2018
Formal methods have been applied in the design of a great number of systems.Many protocols have been specified and verified formally.Some protocol standards are even defined by means of a formal method.This paper studies a based formal approach for testing associated properties of Modbus communication protocol with the Event-B Method.Event-B is a formal method for systems modeling, founded on set theory and predicate logic.It has the benefit of mechanized proof, and it is practicable to model a system in various levels of abstraction using refinement.Our aims are constructing a model with a clear and accurate formulation of the protocol properties and discharge all proof obligations.To satisfy these, attentive choice of invariants and machine theorems was important and eased the proof effort.A major focus of our work has been to explore the use of the Event-B method for formally specifying Modbus protocol.The supported language was sufficiently expressive and all proof obligations could be discharged.We reached a good degree of automatic proof.All interactive proofs involved a small number of steps and were straightforward to reach.The result of this approach was that we achieved a very high degree of automatic proof.