Context-aware approach for formal verification

International audienceThe Context-aware approach has proven to be an effective technique for software model-checking verification. It focuseson the explicit modelling of environment as one or more contexts. In this area, specifying precise requirement is achallenged task for engineer since often environmental conditions lack of precision. A DSL, called CDL, has beenproposed to facilitate the specification of requirement and context. However, such language is still low-level and errorprone, difficult to grasp on complex models and assessment about its usability is still mitigated. In this paper, we propose ahigh level formalism of CDL to facilitate specifying contexts based on interaction overview diagrams that orchestrateactivity diagrams automatically transformed from textual use cases. Our approach highlights the boundaries between thesystem and its environment. It is qualified as model-checking context-aware that aims to reduce the semantic gap betweeninformal and formal requirements, hence the objective is to assist and encourage engineers to put sufficient details toaccomplish effectively the specification process