Lessons learned in a journey toward correct-by-construction model-based development