Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Precise use cases in a context-aware model-checking approach

Amel Benabbou 1 Safia Nait Bahloul 2 Philippe Dhaussy 3
3 Lab-STICC_ENSTAB_ CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
Abstract : Formal verification exhibits well known benefits but comes at the price of formalising precise and sound requirements, what often remains a challenging task for engineers. We propose a high-level formalism for expressing requirements based on interaction overview diagrams, which orchestrate activity diagrams that we automatically derived from use cases. Informal requirements are transformed into scenarios which fuel a context-aware model-checking approach. The approach assumes the availability of a formal model of the system, such as concurrent and communicating automata and a set of requirements specified in the form of contexts, which point out boundaries between the system and its environment. The requirement specification approach blends elaboration and transformation phases. Thanks to this blending, the semantic gap between informal and formal requirements is reduced, while model-checking is improved by contexts modelling. As a consequence, engineers gain support for moving towards formal verification.
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal-ensta-bretagne.archives-ouvertes.fr/hal-01936730
Contributeur : Marie Briec <>
Soumis le : mardi 27 novembre 2018 - 15:40:08
Dernière modification le : mercredi 24 juin 2020 - 16:19:52

Identifiants

Citation

Amel Benabbou, Safia Nait Bahloul, Philippe Dhaussy. Precise use cases in a context-aware model-checking approach. International Journal of Critical Computer-Based Systems, Inderscience, 2018, 8 (3/4), ⟨10.1504/IJCCBS.2018.10017704⟩. ⟨hal-01936730⟩

Partager

Métriques

Consultations de la notice

140