This work presents the tool support for a model-based development methodology for verified software systems. We focus in this discussion on the design, implementation and the verification phase of the overall methodology developed for safety-critical embedded systems. In particular, we show how design models are transformed into C code and Isabelle/HOL theories by code generators. We discuss the applied AutoFocus tool chain and its basic principles emphasizing the verification of the system under development as well as the check mechanisms we applied to raise the level of confidence in the correctness of the implementation of the automatic generators.     «

This work presents the tool support for a model-based development methodology for verified software systems. We focus in this discussion on the design, implementation and the verification phase of the overall methodology developed for safety-critical embedded systems. In particular, we show how design models are transformed into C code and Isabelle/HOL theories by code generators. We discuss the applied AutoFocus tool chain and its basic principles emphasizing the verification of the system unde...     »