Behavioral Verification of UML2.0/PoSM Components

The component approach aims at reutilization by an easy and efficient component assembly. A coherent component assembly requires that the atomic components be correct. Where, an atomic component is said correct if and only if its partial behaviors associated with the interfaces offered by this component are ensured by the global behavior of the said component. In this paper, our purpose was the verification of the behavioral consistency between the interfaces of a component and the component itself. Our proposed approach combined UML2.0, Port State Machine (PoSM), Wright and CSP to check the behavioral consistency of UML2.0/PoSM components. To achieve this, we proposed to translate each UML2.0/PoSM component to a Wright Component. Using Wr2fdr tool, these Wright components were automatically translated to a CSP specification acceptable by the FDR2 model-checker. Thus, the consistency of a component was checked thanks to FDR2.