ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique

APPEL À
CONTRIBUTION
Décisions, argumentation et traçabilité dans l’Ingénierie des Systèmes d’Information
En savoir plus >>
Autres revues >>

Ingénierie des Systèmes d'Information

Networking and Information Systems
1633-1311
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 12/5 - 2007  - pp.133-157  - doi:10.3166/isi.12.5.133-157
TITRE
Mise en œuvre de composants MDA pour la validation formelle de modèles de systèmes d'information embarqués

RÉSUMÉ
L'article présente la définition et l'exploitation d'un concept d'unité de preuve comme élément encapsulant les données nécessaires à la preuve de propriétés sur un modèle de système à vérifier et plongé dans un environnement. Les modèles des unités, manipulées dans le processus de développement, peuvent être construits sous la forme de modèles abstraits à partir des données fournies par les phases d'analyse et de conception du système. Ces modèles intègrent des contextes de preuve abstraits. Ceux-ci modélisent formellement une exigence (ou une composition d'exigences) de sûreté ou vivacité bornée dans un contexte comportemental donné. Dans une approche IDM, les contextes de preuve sont traduits par transformation en modèles concrets puis en codes exploitables par des outils d'analyse formelle. Nous expérimentons cette approche sur une implantation des unités de preuve intégrant une description des contextes de preuve dans un langage nommé CDL et exploités par un outil OBP (Observer-Based Prover) mettant en oeuvre le langage IF et une technique de vérification par observateur.


ABSTRACT
The article presents a work in progress about the definition and the exploitation of a concept of proof unit taken into account to encapsulate all the data necessary to the proof of properties on a model composed with an environment. The models of the units, handled in the process of development, can be built, in the form of abstracted models, starting from the data provided by the phases of analysis and system design. These models integrate abstract contexts of proof. Those formally model a safety or bounded liveness property (or a composition of properties) in a context given. In an MDE approach, the contexts of proof are translated into concrete models then into exploitable codes by tools for formal analysis. We experienced this approach by implementation of the proof units integrating a description of the contexts of proof with a language named CDL and exploited by a tool OBP (ObserverBased Prover) implementing the language IF and a technique of checking with observers.


AUTEUR(S)
Philippe DHAUSSY, Frédéric BONIOL

MOTS-CLÉS
unités de preuve, vérification formelle, observateur, transformation de modèles.

KEYWORDS
proof units, formal checking, observer, model transformation.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (4,63 Mo)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier