ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 31/6 - 2012  - pp.797-826  - doi:10.3166/tsi.31.797-826
TITRE
Formalisation de contextes et d’exigences pour la validation formelle de logiciels embarqués

TITLE
Context and requirement modeling for formal validation of embedded software

RÉSUMÉ

Un des défis posés aux méthodes formelles est leur intégration dans les processus de développement industriel. Une des difficultés rencontrées par les techniques formelles telles que le model-checking est l’explosion de l’espace des états à explorer lors de la vérification. Pour réduire cet espace des états, il est nécessaire de décrire le comportement de l’environnement qui est en interaction avec le système à valider. Cet article s’intéresse à la formalisation de cet environnement que nous nommons « contexte » en lien avec la formalisation des propriétés. Dans ce but, nous proposons et expérimentons un DSL, nommé CDL (Context Description Language) reposant d’une part sur des diagrammes d’activités et de séquences pour l’expression du comportement de l’environnement, et d’autre part sur la notion d’observateur pour l’expression des propriétés à vérifier. Afin de contourner l’explosion des états produite par la composition des modèles de l’environnement et du système à valider, nous appliquons une technique de partitionnement du comportement de l’environnement en sous-contextes analysables séparément. Nous illustrons notre contribution par un exemple, et présentons les retours d’expérience obtenus sur six cas d’études industriels.



ABSTRACT

This paper deals with the problem of the usage of formal techniques, based on model checking, where models are large and formal verification techniques face the combinatorial explosion issue. The goal of the approach is to express and verify requirements relative to certain context situations. The idea is to unroll the context into several scenarios and successively compose each scenario with the system and verify the resulting composition. We propose to specify the context in which the behavior occurs using a language called CDL (Context Description Language), based on activity and message sequence diagrams. The properties to be verified are specified with textual patterns and attached to specific regions in the context. This article shows how this combinatorial explosion could be reduced by specifying the environment of the system to be validated. Our contribution is illustrated on an industrial embedded system.



AUTEUR(S)
Philippe DHAUSSY, Frédéric BONIOL, Jean-Charles ROGER, Amine RAJI, Yves LE TRAON, Benoit BAUDRY

MOTS-CLÉS
vérification, contexte, scénarios, cas d’utilisation, patrons de propriétés

KEYWORDS
verification, context, scenarios, use cases, property pattern.

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  (878 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier