Back-annotation of Execution Sequences by Advanced Search and Traceability Techniques

The advance of information technology gives rise to software systems with an ever increasing level of complexity. In order to find design errors in such systems, the analysis of their functional and non-functional properties are required from an early phase of design.

Model-driven engineering facilitates the systematic use of models as the main artifacts in  the development and analysis of complex systems. High-level domain-specific models (such as SysML, AADL, MARTE or BPEL) are created to represent the software or hardware architecture, dynamic behavior or quality attributes of systems.

In the field of safety critical systems even a minor design error can lead to catastrophic failures. In case of business critical systems, such failures may lead to severe financial losses. Therefore, formal methods are often applied to ensure the correctness of the design before actual development and deployment.  

In \emph{model-based analysis} domain-specific models are transformed automatically into formal models to find design errors in the system early in the development process. The verification of these formal models is carried out based on a system requirements and the results can support the designer in correcting or improving the system design. For behavioral models, the analysis results are often presented as a counter-example, which is an execution sequence representing the dynamic execution of the system.

There is a ``semantic gap'' between the high-level domain models and the analysis results since systems engineers and business analysts are often not familiar with the exact details of the formal models. To bridge this gap and provide feedback on the right level, the results must be back-annotated to the domain model using traceability information between the domain and formal models.

Therefore, this dissertation is centered around providing novel techniques for (i) automated \emph{back-annotation of execution sequences} for behavior models through the application of (ii) robust traceability methods using soft interconnection of model fragments and (iii) guided design space exploration techniques for search-based problems. While the methods defined for (ii) and (iii) are both applicable by themselves, they also support and enable the proposed back-annotation approaches.  

My contributions of the thesis are the following, (a) I define back-annotation methods between execution sequences of behavior models using a model-based representation and a generic replaying framework. I specify two back-annotation approaches, the first based on change-driven model transformations and another using design space exploration.
The back-annotation of execution sequences requires specific techniques for exploring possible domain sequences, therefore (b) I define a guided design space exploration approach where hints obtained by system analysis are interpreted during the exploration to increase the efficiency of the search using selection and cut-off criteria. 
The domain and formal models are connected by traceability links and to support approaches that depend on traceability, (c) I propose soft interconnections driven by incrementally evaluated model queries as a technique for providing robust traceability links between model fragments. 

The results of this dissertation are integrated into the Design Space Exploration component of the Viatra framework and the query-driven derived feature support of EMF-IncQuery. The end-to-end business process verification tool was developed as part of the Sensoria European Union FP6 research project, while soft interconnections were successfully applied in a research collaboration with Embraer.