Good implementation of systems (especially those supporting critical applications) alone does not assure that a proper quality of service will be delivered by the system in operations. From the very early stages of the design process, an early validation of concepts and architectural choices (without wasting time and resources in the realization phase) is essential to understand whether the required quality of service will be delivered. Dependability (covering reliability, availability, safety) is one of the parameters to be validated, especially in systems required to provide continuous and/or critical services. The use of formal methods for the validation of properties is one methodological improvement of the system production process. However, the need of the knowledge of sophisticated mathematical formalisms and techniques prevented the wide adaptation of formal methods. Our approach hides the background mathematics for the designer by (i) providing a set of transformations from the high-level visual model to the formal model and (ii) automatic back-annotation of the results. In this way, by methodological or automatic derivation of formal models we contribute in making the dependability evaluation by application of formal methods more a discipline than an art.