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.
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: 22 Nov 2018 *