Résumé
The IDCM framework (Incremental Development of Conforming Models) supports incremental constructions and evaluations of UML behavioral models (architecture of components and state machines). This framework evaluates models with respect to implicit temporal safety and liveness properties. The specifiers and designers only describe models, they don't need to write down explicit temporal logic properties. In this paper, we show how explicit safety and liveness properties can also be described using semi-formal boilerplates, translated into classical temporal logic formulas which are themselves translated into testing transition systems. Adding evaluation means to model-based development (relation checking) is a way to develop models incrementally, following a spiral-based development cycle.