A UML-based complex system design method MoFoV (Modeling/Formalizing/Verifying)

This article presents a support method for the design of complex systems. This approach, (named MoFoV for Modeling/Formalizing/Verifying) is devoted to a functional view of systems. Assigned to technological contexts, this method is based on two generic models (which vary depending on each specific application domain). The first (MOGET) is dedicated to systems treatments (in terms of functions) whilst the second (MOGEP) deals with the potential properties of those systems. These generic models can be specialized (using the functional and non-functional requirements, extracted from the specification document) in order to represent an exact solution (treatments oriented) to the expected requirements. Both specific models must be formalized (in term of homogeneity, consistency, architecture and modeling rules) before being tested with formal proof tools (for example the Model Checker SMV). We show the positioning and the global orientations of such a design support method. Then, it will be possible to clarify what this method needs in order to run and how it can practically be used. Finally, this system design method aims to improve the relationship between the modeling (from requirements) and formal verification task indeed, these phases are usually separated and are rarely commonly integrated in a design process.