IDF: A framework for the incremental development and conformance verification of UML active primitive components

• We give an efficient support to design and verify UML state machine models.
• We propose an Incremental Development Framework providing formal model evaluations.
• Compliant models are built step-by-step, by preserving liveness properties.
• We select relevant conformance relations for extension, refinement and increment.
• We provide a tool to support the incremental development of models.

Modelling component behaviour is widely recognised as a complex task during the specification and design phases of reactive systems. Our proposal for treating this problem involves an incremental approach that allows UML state machines to be built using a composition of two types of development: model extension for adding services or behaviours, and refinement for adding details or eliminating non-determinism. At each step of the development process, the current model is verified for compliance with the model obtained during the previous step, in such a way that initial liveness properties are preserved. The novelty of this work lies in the possibility to combine and sequence both refinement and extension developments. This iterative process is usually not taken into account in conventional refinement relations. This set of development techniques and verification means are assembled into a framework called IDF (Incremental Development Framework), which is supported by a tool, under the acronym IDCM (Incremental Development of Compliant Models), developed herein in addition to the Topcased UML tool.