Refinement, verification in component-based model-driven design