Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

USER CONTEXT MODELS : A FRAMEWORK TO EASE SOFTWARE FORMAL VERIFICATIONS

Abstract : Several works emphasize the difficulties of software verification applied to embedded systems. 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 remains 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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-00471931
Contributeur : Amine Raji <>
Soumis le : vendredi 9 avril 2010 - 16:10:18
Dernière modification le : vendredi 13 décembre 2019 - 10:42:04
Archivage à long terme le : : samedi 10 juillet 2010 - 20:45:11

Fichier

ICEIS_2010_CR_version.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00471931, version 1

Collections

Citation

Amine Raji, Philippe Dhaussy. USER CONTEXT MODELS : A FRAMEWORK TO EASE SOFTWARE FORMAL VERIFICATIONS. 12th International Conference on Enterprise Information Systems, Jun 2010, Funchal, Madeira, Portugal. pp.1. ⟨hal-00471931⟩

Partager

Métriques

Consultations de la notice

432

Téléchargements de fichiers

417