A process for improving multi-technology system high level design: modeling, verification and validation of complex optronic systems

In order to support the design of complex systems such as optronic systems, and especially the function-processing oriented part of this work, we propose a method based on a connection of stages. This is aimed at making the representation of the system and its properties both formal and checkable. These formalizations can be used to manage the real verification of the system and determine the agreement between its model and the expected properties. The principle is to follow the first steps (corresponding to the design phase) of the traditional V-cycle of system development, and to enrich each step with formal features: the first step is the elaboration, based on initial requirements, of a function processing oriented specification. The first result is then a formalized (functional and non-functional) requirements set. It allows the system designer to construct, using the generic model and properties inventory, the precise model of the system (i.e. an instantiated model, called MOTI), and the list of properties to be verified. This MOTI is then (automatically) translated into a so-called MOTIF expressed in a formalism dedicated to formal proof (required for formal verification and validation processes). Concurrently, the expected properties (which have been extracted from the generic properties inventory enriched by specific characteristics such as user-defined values or application-specific parameters), are translated into the accurate formalism for automated proof