Credible autocoding and model-based control design and validation - Eric Feron