Article Preview
TopIntroduction
In Model-checking, the System Under Study (SUS) is abstracted as a whole model, presented in the form of concurrent automata. The objective is to verify the correctness of requirements described in a formal properties language. Furthermore, in context-aware model-checking technique; the SUS model is separated from the set of behaviours of its environment (the set of actors). The context-aware technique focuses on modelling the system environment as a set of particular use cases scenarios, called Contexts. This technique has been introduced to solve the problem of explosion of the state space (Pelanek, 2009) by decreasing the set of possible behaviours. Thus, the SUS is closed with a well-defined finite and acyclic environment. Based on this idea, an approach has been proposed in (Dhaussy et al., 2012) within a verification methodology. In such approach, the SUS is modelled using Fiacre language (Berthomieu et al., 2008), which enables the specification of the interacting behaviours and constraints through automata. The surrounding environment in form of contexts is specified using the CDL (Context Description Language) (Dhaussy & Roger, 2011). Properties are formalized (also within CDL) to be checked on the SUS model using the model-checker OBP (Observer Based Prover) (http://www.obpcdl.org). See Figure 1.
Figure 1. Context-aware verification approach: OBP Observation engine overview
CDL is a domain-specific language based on the concept of contexts and used for the formal specification of the SUS environment. The CDL structure is inspired from the Use Case Chart proposal (Whittle, 2006) and is hierarchically constructed in three levels: Level-1 is a set of use cases diagrams which describes hierarchical activity diagrams where either alternative (alternative/merge) or parallelization (fork/join) between several executions is available. Level-2 is a set of scenario diagrams organized by alternatives. Each scenario is fully described at Level-3 by UML2 sequence diagrams. Level-1 and Level-2 are based on the semantic of the scenarios and expressed using seq (;), alt ([]) and par (||) operators (par only for Level-1). At Level-3, the semantic of a scenario is expressed by a set of traces (sequence of ordered events) as described in (Haugen et al., 2005) and according to the semantics of UML 2 sequence diagrams. See Figure 2.
Figure 2. An example of CDL Model: Graphical Vs Textual version
Within a CDL specification, the behaviour of each actor is considered as a set of use cases scenarios. The users are then required to identify the behaviour of each actor to formalize it in a CDL scenario. This manual process is a difficult and error prone task for engineers without formal methods background, furthermore, it requires: a) significant effort, especially when the system is strongly coupled with its environment; b) good knowledge of the syntax and semantics of CDL. Moreover, there is a semantic gap between the textual description of the use cases and CDL models that technically capture the messages exchanged between the system and its environment. Also, CDL has been evaluated through several industrial case studies (Dhaussy et al., 2009). However, the feedback reports that although it has solved several state explosion cases, it is perceived as a low-level language and difficult to grasp on complex models. Then, one need to express environmental scenarios at a higher level of abstraction that maps better to engineers. This aims to facilitate contexts elaboration and build intermediate models between textual format of use cases and CDL specifications. From these high-level artefacts, CDL models are later generated automatically.