Eclipse Formal Modeling Project

The symbolic execution platform of the E-FMP project will be organized around a symbolic execution infrastructure as illustrated in Figure 1. 

Figure 1. The symbolic execution platform of the E-FMP project 

a.       All the steps of the symbolic execution processing in this infrastructure can be customized by adding modules specific to a kind of formal analysis. Many such modules are already available in DIVERSITY: modules to highlight live-locks, deadlocks, bad synchronizations between sub-systems; modules to check predicates; and modules to generate test cases and compute test verdicts [4] [5] [6].

b.       In order to make use of the (existing) formal analysis modules, input models are meant to be expressed with the xLIA pivot language. As glimpsed at the beginning of the section, xLIA has proven its flexibility to capture various semantics. Some of the targeted modelling formalisms are state-based notations, communicating process languages, scenario-oriented notations, etc. In order to enable transparent usages of the formal analysis modules for non-experts of formal methods, users may access to a catalogue of import gateways. Those gateways permit to edit models in user-friendly environments. Advanced users may develop their own import gateways. For instance, a gateway from a subset of UML/SysML using model transformation techniques has been developped by the CEA as a plug-in for Papyrus [7] which is an Eclipse integrated modeling environment. It allows analyzing sequence diagram models [8] [9].

c.       Similarly to import gateways, export gateways can be developed. Those gateways are used to export the results of the analysis towards specific modeling environment. For instance, a gateway has been developed in order to export test cases computed by DIVERSITY to TTCN-3 [2]. Again, advanced users may develop their own export gateways. 

The symbolic execution infrastructure (SE for short) is a central component of the symbolic execution platform of the E-FMP project . In paragraph A, we describe its structuration (which reflects the architecture of the DIVERSITY kernel) and we emphasize all its customization possibilities. In paragraph B, we present the formal analysis functionalities that have been implemented in this infrastructure and that will be made available at the initial release. Similarly in paragraph C, we introduce the import/export gateways that will be made available as well.  

A. Customizable symbolic execution infrastructure

Symbolic execution consists in computing the semantics of a model/program (in the sequel we simplicity talk about a model) in an abstract manner by constraint propagation on input symbolic values. The result of the symbolic execution is a tree-like structure where a path abstracts a class of concrete execution of the analyzed object. Symbolic trees are potentially infinite structures due to the possibility of repeatedly executing an unbounded loop for example. Classically, SE allows setting stopping criteria related to the tree size. Once such a symbolic tree is computed, SE provides post processing facilities to conduct formal analysis on the symbolic tree. In addition, the SE infrastructure has been designed so as to allow customized formal treatment on the fly during the construction of the symbolic tree. We will discuss in the remaining of the section, the entry points offered by the SE infrastructure to access on the fly the generic symbolic execution processing in order to insert new formal treatments. 

Figure 2. The running process of the symbolic execution platform

The symbolic processing consists of five Steps (i), …, (v) depicted in Figure 2. The scheduling of these steps is cyclic. Each cycle consists in updating a queue of so-called Execution Contexts, denoted ECs. Intuitively, an EC fully characterizes a class of executions (all those who follow a common path in the model control graph) and is defined by the following pieces of information:

• [Data part] the set of symbolic values ​​associated with variables of the model; and a path condition consisting in a conjunction of constraints on those symbolic values; The path condition fully characterizes the constraints to be satisfied in order to follow the path associated to the EC.
• [Control part] the control points of the model control graph reached at the end of the executions characterized by the EC.

At the beginning of the first iteration of the cycle, the queue contains one EC which characterizes the initial symbolic values associated with the variables and the path condition is restricted to True because no constraint has not yet been encountered. Each iteration step consists in: selecting one or more EC(s) (removed from the queue); computing their children ECs by symbolically executing all possible atomic instructions subsequent to the control points reached in the parent ECs; deciding whether or not the parent ECs are added to the tree; in which case, their children ECs are added in the queue. The whole symbolic processing is based on the notation of the so-called filter. The purpose of a filter is to dynamically accept or reject ECs according to a specific user coverage purpose. It can be seen as a selection strategy to complement the traversal strategy in order to increase the chances of reaching the targeted coverage while avoiding combinatorial explosion. The processing is detailed as follows:

Step (i): Selection of EC candidates for Step (ii)

One or more EC are selected from the queue according to a customizable strategy. For the moment, the following exploration strategies for generating the symbolic tree are implemented: Random traversal, classical BFS (Breadth First Search) and DFS (Depth First Search) traversals. Some heuristics may however associate a weight with each of the EC, and thus induce an order thereof in the queue which becomes a priority queue. 

Step (ii): Pre-filtering

Pre-filtering consists in applying one or more filters to reason on ECs before computing their children. If the EC successfully passes the scrutiny of each of the chained filters, it continues its way in the symbolic processing flow, through Step (ii-a). Otherwise Step (ii-b), the EC will be ignored or possibly tagged (by an informative note on the reason for its failure) and inserted into the symbolic tree under construction. In the favorable case where all user coverage objectives are met, the symbolic processing stops.

Step (iii): Symbolic execution

Each EC issued from Step (ii-a) is evaluated symbolically. During the evaluation its children EC1, ..., ECn are computed. For example, in the context of classical state-machines, it consists in symbolically executing outgoing transitions from active states indicated by the control part of the EC. For each transition, the newly computed child EC denotes:

• New symbolic values ​​associated with state-machine variables after executing the assignment of the transition and applying the communication rules;
• New path condition computed by taking into account the guard of the transition;
• New active states being targets of the transition effectively evaluated.

More information can be kept in the EC. For example, the evaluated transitions can be saved in each of the children ECs together with the (symbolic) input/output sequences which result from the symbolic evaluation of the communication actions.

Step (iv): Post-filtering

Step (iv) is similar to Step (ii), except that the filter involved in post-filtering reasons on the EC and its children to decide of the future of the symbolic processing. After passing the post-filters, there are two possibilities:

• Step (iv-a) If successful, the symbolic processing continue with Phase (v) in which case the the EC is added to the tree.
• Step (iv-b) If failed, the EC and its children EC1, ..., ECn are ignored or inserted in the symbolic tree (possibly tagged by an informative note on the reason for their failure);

As in Step (ii), in the favorable case where all user coverage objectives are met, the symbolic processing stops.

Step (v): All the children EC1, ..., ECn resulting from Step (iv-a) are enqueued and the symbolic processing iterates with Step (i).  

B. Modules of formal functionalities

Formal functionalities are implemented in the SE infrastructure using the filter mechanism. The formal functionalities available at the beginning of the E-FMP project will be:

Verification of predicates: These functionalities allow passive verification of the usual boolean predicates on variables, extended to communication actions. The verification occurs on the fly on each execution context EC built by the symbolic processing. This functionality acts as a passive observer not influencing the symbolic processing.

Hit-or-Jump exploration strategy: Classical search algorithms like Breadth First Search (BFS) are implemented in the SE infrastructure. However in some cases, using BFS results in exploring a large number of paths in the symbolic tree which are irrelevant to the coverage criteria. The SE infrastructure implements an adaptation of the heuristic traversal called Hit-or-Jump [11]. This heuristics aims at computing a symbolic tree covering a declared sequence or set of transitions. The idea is to define a maximal depth N for which a symbolic tree is computed in BFS manner. Once it is computed, an analysis is realized to study whether or not a part of the tree satisfies the coverage: (Hit) If some non-empty prefixes of the sequence has been covered, the set of paths that have covered the greatest prefix are identified, and then one or several ones among them are chosen at random, else one or several paths are chosen at random; (Jump) Once a path is chosen the whole process starts again from the last symbolic state of the path (i.e. the target state of the last symbolic transition of the path) until the sequence is fully covered.

Eliciting unitary behaviors: In a component oriented approach, components are designed, developed and validated in order to be widely used. However one cannot always foresee which specific uses will be made of components depending on the system they will constitute. The SE infrastructure provides a filter implementing the approach in [5] whose goal is extract accurate component behaviors using information given by the system specification. By projecting symbolic execution of a system on its components, unitary symbolic component behaviors are derived from symbolic system behaviors. In practice, those component behaviors can be seen as typical behaviors of the component in the context of the system.

Off-line Test Case Generation: Model-based conformance testing of reactive systems consists in taking advantage of the model for mechanizing both test data generation and verdicts computation. In off-line approaches, test suites are pre-computed from the model and stored to be later performed on test-beds. The SE infrastructure implements two filters, one for test case generation and one for verdict computation, both of them based on the work presented in [6]. A generated test case is a timed sequence of numerical stimuli data and waiting delays. This sequence is intended to be submitted to the System Under Test (SUT), and then the timed sequence of output data resulting from the corresponding execution of the SUT is post-processed according to the model to deliver a test verdict. 

C. Functionalities of import/export

The following import/export functionalities will be available in E-FMP project:

Import of UML scenario models: Imported scenario models are described by means of a subpart of UML sequence diagrams (enriched with timing properties expressed in VSL language from the UML profile MARTE [12]). Sequence diagrams are translated into Timed Input Output Symbolic Transition Systems (TIOSTS) [8] which are symbolic automata that can be encoded straightforwardly in xLIA. The symbolic semantics has been given in practice by a model transformation and has been implemented as a plug-in for Papyrus [7]. A typical usage scenario is to analyze system specification to extract test cases that can be later exploited by the offline testing filters presented in Section 3.2. This usage scenario has been experimented with several cases studies [13] [14]. 

Export test cases in TTCN-3 format: A path in the symbolic tree represents the intended sequence of input/output communication actions between the SUT and its environment. From such paths, numeric sequences of inputs and outputs are computed using constraint solving techniques on path conditions. The SE infrastructure allows this treatment and provides a filter permitting to export these sequences in the form of TTCN-3 test cases (refer to the work in [2] for a practical usage of this gateway).