Contracts-refinement proof system for component-based embedded systems