En depit de l'efficacite des methodes formelles, en particulier les techniques d'analyse de modeles (model checking), a identifier les violations des exigences dans les modeles de conception, leur utilisation au sein des processus de developpement industriel demeure limitee. Ceci est du principalement a la complexite des modeles manipules au cours de ces processus (explosion combinatoire) et a la difficulte de produire des representations formelles afin d'exploiter les outils de verification existants. Fort de ce constat, mes travaux de these contribuent au developpement d'un volet methodologique definissant les activites conduisant a l'obtention des artefacts formels. Ceux-ci sont generes directement a partir des exigences et des modeles de conception manipules par les ingenieurs dans leurs activites de modelisation. Nos propositions s'appuient sur les travaux d'exploitation des contextes pour reduire la complexite de la verification formelle, en particulier le langage CDL. Pour cela, nous avons propose une extension des cas d'utilisation, afin de permettre la description des scenarios d'interaction entre le systeme et son environnement directement dans le corps des cas d'utilisation. Aussi, nous avons propose un langage de specification des exigences base sur le langage naturel controle pour la formalisation des exigences. Cette formalisation est operee par transformations de modele generant des proprietes CDL formalisees directement des exigences textuelles des cahiers des charges ainsi que les contextes CDL a partir des cas d'utilisations etendus. L'approche proposee a ete instanciee sur un cas d'etude industriel de taille et de complexite reelles developpees par notre partenaire industriel.

Un des defis poses aux methodes formelles est leur integration dans les processus de developpement industriel. Une des difficultes rencontrees par les techniques formelles telles que le model-checking est l'explosion de l'espace des etats a explorer lors de la verification. Pour reduire cet espace des etats, il est necessaire de decrire le comportement de l'environnement qui est en interaction avec le systeme a valider. Cet article s'interesse a la formalisation de cet environnement que nous nommons " contexte " en lien avec la formalisation des proprietes. Dans ce but, nous proposons et experimentons un DSL, nomme CDL (Context Description Language) reposant d'une part sur des diagrammes d'activites et de sequences pour l'expression du comportement de l'environnement, et d'autre part sur la notion d'observateur pour l'expression des proprietes a verifier. Afin de contourner l'explosion des etats produite par la composition des modeles de l'environnement et du systeme a valider, nous appliquons une technique de partitionnement du comportement de l'environnement en sous-contextes analysables separement. Nous illustrons notre contribution par un exemple, et presentons les retours d'experience obtenus sur six cas d'etudes industriels.

The complexity of image processing algorithms using mathematical calculations grows from the nature of the image to be processed and the desired result. A hardware implementation of these algorithms for the needs of real-time and embedded systems improves performances. In this paper we present some existing approaches used for hardware systems modeling. We propose a new graphical tool for designing image and video processing embedded systems called VIP DESIGN (Video and Image Processing Design). The novelty of our approach is that we bypass the shortcomings of existing languages by providing a high level of abstraction through two kinds of diagrams: structural diagram and filter edition diagram. It also allows formal verification and automatic code generation for ASIC and FPGA implementation.

Despite technical improvements in current verification tools, the increasing size of developed systems makes the detection of design defects more difficult. Context-aware Model-Checking is an effective technique for automating software verifications considering specific environmental conditions. Unfortunately, few existing approaches provide support for this crucial task and mainly rely on significant effort and expertise of the engineer. We previously proposed a DSL (called CDL) to facilitate the formalization of requirements and contexts. Experiences has shown that manually writing CDL models is difficult and error prone task. In this paper, we propose a tool-supported framework to automatically generate CDL models using eXtended Use Cases (XUC). XUC models consistently link use cases with scenarios with respect to the domain specification vocabulary of the model to be checked. We also propose a requirements specification language to fill the gap between textual requirements and CDL properties. An industrial case study is presented to illustrate the effectiveness of XUCs to generate correct and complete CDL models for formal model analysis.

The complexity of image processing algorithms using mathematical calculations grows from the nature of the image to be processed and the desired result. A hardware implementation of these algorithms for the needs of real-time and embedded systems improves performances. In this paper we present some existing approaches used for hardware systems modeling. We propose a new graphical tool for designing image and video processing embedded systems called VIP DESIGN (Video and Image Processing Design). The novelty of our approach is that we bypass the shortcomings of existing languages by providing a high level of abstraction through two kinds of diagrams: structural diagram and filter edition diagram. It also allows formal verification and automatic code generation for ASIC and FPGA implementation.

Formal methods are effective techniques for automating software verifications to satisfy quality and reliability. However, the application of these techniques within industrial settings remains limited due to the (i) complexity of the models that have to be checked and (ii) the difficulty to produce formal artifacts required by existing formal verification tools. Context-aware verification can circumvent (i) by reducing the scope of the verification to some specific environmental conditions (contexts). Model driven development can help to handle (ii) thanks to model transformations and formal code generators. In this paper, we propose a methodological approach to help engineers to apply formal verifications in industrial settings. In our approach we propose a set of user oriented models to ease the capture and formalization of requirements and contexts to generate required formal artifacts directly from high level user models.

Formal methods are effective techniques for automating software verifications to satisfy quality and reliability. However, the application of these techniques within industrial settings remains limited due to the complexity of produced models. Context-aware verification can circumvent this complexity by reducing the scope of the verification to some specific environmental conditions. We previously proposed a Context Description Language (CDL) to facilitate the formalization of requirements and contexts. However, the number of CDL models required to precisely formalize contexts grow rapidly according to the complexity of the system and manually writing CDL models is difficult and error prone task. In this paper, we propose a tool-supported framework that assists engineers in describing system contexts. We extended UML use cases with scenarios descriptions and we linked a domain specification vocabulary to automatically generate CDL models. An industrial case study is presented to illustrate the effectiveness of our approach.

Context-aware veri cations are e ective techniques for au- tomating software veri cations considering speci c environ- mental conditions. Unfortunately, few existing approaches provide support for this crucial task and mainly rely on sig- ni cant e ort and expertise of the engineer. We previously proposed a DSL (called CDL) to facilitate the formaliza- tion of requirements and contexts. Experiences has shown that the number of CDL models required to precisely for- malize contexts grow rapidly according to the complexity of the system and manually writing CDL models is di cult and error prone task. In this paper, we propose a tool-supported framework that assists engineers in describing system con- texts using eXtended Use Cases (XUC). XUC models con- sistently link use cases with scenarios with respect to the domain speci cation vocabulary of the model to be checked. An industrial case study is presented to illustrate the ef- fectiveness of XUCs to generate correct and complete CDL models for formal model analysis.

Au cours de ces six dernieres annees, nous nous sommes interesses a la problematique d'integration des techniques de verification formelles de type model checking aux processus de developpement industriel en tirant profit de l'Ingenierie Dirigee par les Modeles. Nous avons propose et evalue un langage (nomme CDL) permettant de formaliser les proprietes ainsi que le comportement de l'environnement du modele a valider pour faciliter la manipulation des outils de verification formels et limiter le probleme de l'explosion combinatoire. Les resultats ont ete prometteurs (Dhaussy et al., 2009), mais la manipulation de CDL dans un cadre industriel souffre du manque du cadre methodologique et constitue une rupture semantique avec les modeles manipules, jusqu'alors, dans les processus industriels. Dans cet article, nous proposons une solution a ce probleme a travers la definition de modeles, orientes utilisateurs, permettant de faire cette jonction.

Formal methods have increasingly been recognized as effective techniques for automating software verifications to satisfy quality and reliability. However, using such techniques within industrial development processes takes an important part of the development time and budget due to the complexity of developed software. Context aware techniques can circumvent this complexity by reducing the scope of the verification to some precise system configurations. Unfortunately, few existing approaches provide support for this crucial task and mainly rely on significant effort and expertise of the engineer. In this paper, we propose a tool-based framework that automate the description of the system contexts to improve the integration of formal verification techniques into industrial engineering methods. Models describing contexts are automatically generated from use cases and scenarios using model transformations. Then, requirements are checked considering generated contexts to reduce the complexity of the proof.

Several works emphasize the difficulties of software verification applied to embedded systems. In industrial development practices, the verification process takes a great part of the development time and budget to satisfy quality and reliability. In past years, formal verification techniques and tools were widely developed and used by the research community. However, the use of formal verification at industrial scale still difficult, expensive and requires lot of time. This is due to the size and the complexity of manipulated models, but also, to the important gap between requirement models manipulated by different stackholders and formal models required by existing verification tools. In this paper, we fill this gap by providing the UCM framework to automatically generate formal models used by formal verification tools. At this stage of our work, we generate behavior models of environment actors interacting with the system directly from an extended form of use cases. These behavioral models can be composed directly with the system automata to be verified using existing model checking tools.

In his article paper entitled "From Play-In Scenarios to Code: An Achievable Dream",David Harel presented a development schema that makes it possible to go fromhigh-level user-friendly requirements to a full system model, andfrom there to the final implementation.Even if Harel's schema represents a real contribution to filing the gapbetween user requirements and final implementations, there is few work onits feasibility and none within UML2.This paper addresses this lack. First we use UML2 sequence diagrams as a formalism forrequirement specification. Thenan approach that synthesizes state machinesfrom UML2 sequence diagrams is presented. From the obtained state machines, weimplementa transformation to code. The AIBO platform (one of several typesof robotic pets designed and manufactured by Sony) is used as a case study toillustrate our implementation.

A well known challenge in the formal methods domain is to improve their integration with practical engineering methods. In the context of embedded systems, model checking requires first to model the system to be validated, then to formalize the properties to be satisfied, and finally to describe the behavior of the environment. This last point which we name as the proof context is often neglected. It could, however, be of great importance in order to reduce the complexity of the proof. The question is then how to formalize such a proof context. We experiment a language, named CDL (Context Description Language), for describing a system environment using actors and sequence diagrams, together with the properties to be checked. The properties are specified with textual patterns and attached to specific regions in the context. Our contribution is a report on several industrial embedded system applications.