Formalization and Refinement Proof for Embedded Systems

This article deals with the verification of refinement of embedded systems. It's about demonstrating the correctness of the refinement engendered by transformations written in Pomset. This will allow, thereafter, the design of correct systems by construction. The principle of our formal verification approach of refinement is to benefit from the power of transition system for the formal verification. For that, we propose an algorithm allowing the passage from Pomsets to Labelled Transition system (LTS), on which we can apply algorithms of formal verification of refinement which already exist. Then, we validate our approach, applying it to the communication refinement transformation.