The problem of configuring a variability model is widespread in many different domains. Renault has developed its technology internally to model vehicle diversity. This technology relies on the approach known as knowledge compilation to explore the configurations space. However, the growing variability and complexity of the vehicles’ range hardens the space representation problem and may impact performance requirements. This paper tackles these issues by exploiting symmetries that represent isomorphic parts in the configuration space. The extensive experiments we conducted on datasets from Renault show our approach’s robustness and effectiveness: the achieved gain is a reduction of 52.13% in space representation and 49.81% in processing time on average.

The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state space generation, computation of global properties, computation of some upper bounds in the model, evaluation of reachability formulas, evaluation of CTL formulas, and evaluation of LTL formulas. For each examination and each model instance, participating tools are provided with up to 3600 s and 16 gigabyte of memory. Then, tool answers are analyzed and confronted to the results produced by other competing tools to detect diverging answers (which are quite rare at this stage of the competition, and lead to penalties). For each examination, golden, silver, and bronze medals are attributed to the three best tools. CPU usage and memory consumption are reported, which is also valuable information for tool developers.

This paper presents a Software Product Line (SPL) extraction approach to handle legacy software systems running on the Java Virtual Machine (JVM), for which the source code is unavailable, and factor in all input programming languages for the JVM. The approach extracts from the bytecode of a collection of software variants created using the Clone-And-Own approach a full SPL with its feature model. We provide a full implementation and integration in the BUT4Reuse framework. An early experiment was carried out on the ArgoUML case study and preliminary results are discussed.

While Service Oriented Architectures (SOAs) are for many parts deployed online, and today often in a cloud, the testing of the systems still happens mostly locally. In this paper, we want to present the MIDAS Testing as a Service (TaaS), a cloud platform for the testing of SOAs. We focus on the testing of whole SOA orchestrations, a complex task due to the number of potential service interactions and the increasing complexity with each service that joins an orchestration. Since traditional testing does not scale well with such a complex setup, we employ a Model-based Testing (MBT) approach based on the Unified Modeling Language (UML) and the UML Testing Profile (UTP) within MIDAS. Through this, we provide methods for functional testing, security testing, and usage-based testing of service orchestrations. Through harnessing the computational power of the cloud, MIDAS is able to generate and execute complex test scenarios which would be infeasible to run in a local environment.

Behavior Model Inference techniques aim at mining behavior models from execution traces. While most of approaches usually ground on local similarities in traces, recent work, referred to as behavior mining with temporal steering, propose to include long term dependencies in the mining process. Such dependencies correspond to temporal implications between events in execution traces, whose consideration allows to ensure a better consistency of the extracted model. Nevertheless, the existing approaches are usually limited by their high computational complexity and the approximations to reduce the cost of temporal rules checking. This paper revisits behavior mining with temporal steering by defining an efficient algorithm that performs an exact consideration of the observed dependencies: in our experiments, greatly reduced processing times (from exponential to quasi-linear) for exact mining with temporal steering have been observed. Furthermore, beyond highlighting the great benefits of considering temporal dependencies, this paper also proposes new key extensions to the existing work that allow to include more complex dependencies in the mining process. Intensive evaluation finally demonstrates the great performances of the proposed approach.

Controller synthesis consists in automatically generating a controller to restrict a hardware or software system so that it respects given requirements, for instance safety properties. Existing synthesis tools for discrete event systems mainly solve the problem for systems described in low-level formalisms.

CosyVerif aims at gathering within a common framework various existing tools for specification and verification. It has been designed in order to 1) support different formalisms with the ability to easily create new ones, 2) provide a graphical user interface for every formalism, 3) include verification tools called via the graphical interface or via an API as a Web service, and 4) offer the possibility for a developer to integrate his/her own tool without much effort, also allowing it to interact with the other tools. Several tools have already been integrated for the formal verification of (extensions of) Petri nets and timed automata.

Reverse engineering of behavior models has received a lot of attention over the last few years. However, no standard benchmark exists for the comparison and analysis of published miners. Evaluation is usually performed on few case studies, which fails to demonstrate effectiveness in a broad context. This paper proposes a general, approach-independent, platform for the intensive evaluation of behavior miners. Its goals are essentially: provide a benchmark mechanism for reverse engineering; allow analysis of miners w.r.t. a class of programs and/or behaviors; help users in choosing the best suited approach for their objective.

The reverse engineering of behavioral models consists in extracting high-level models that help understand the behavior of existing software systems. In the context of reverse engineering of sequence diagrams, most approaches strongly depend on the static analysis and instrumentation of the source code to produce correct diagrams that take into account control flow structures such as alternative blocks ("if"s) and repeated blocks ("loop"s). This approach is not possible with systems for which no source code is available anymore (e.g. some legacy systems). In this paper, we propose an approach for the reverse engineering of sequence diagrams from the analysis of execution traces produced dynamically by an object-oriented application. Our approach is fully based on dynamic analysis and reuses the k-tail merging algorithm to produce a Labeled Transition System (LTS) that merges the collected traces. This LTS is then translated into a sequence diagram which contains alternatives and loops. A prototype of this approach has been tested with a real world application that has been developed independently from the present work. Our results show that this approach can produce sequence diagrams in reasonable time and suggest that these diagrams are helpful in understanding the behavior of the underlying application.