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

Authors: Amel Benabbou; Safia Nait-Bahloul; Philippe Dhaussy

Addresses: Litio Laboratory, University Oran1 Ahmed Benbella, BP 1524, El-M'Naouer, Oran, 31000, Algeria ' Litio Laboratory, University Oran1 Ahmed Benbella, BP 1524, El-M'Naouer, Oran, 31000, Algeria ' Lab-STICC Laboratory, MOCS Team, ENSTA Bretagne, Brest, 29000, France

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.

Keywords: model-checking; context; use cases; interaction overview diagram; IOD; context-aware verification.

DOI: 10.1504/IJCCBS.2018.096440

International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.3/4, pp.371 - 406

Received: 21 Aug 2017
Accepted: 26 Jun 2018
Published online: 30 Nov 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article