Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2013 | Book

Variability in Software: State of the Art and Future Directions Read chapter Read first chapter

Fundamental Approaches to Software Engineering

16th International Conference, FASE 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings

Editors: Vittorio Cortellessa, Dániel Varró

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book constitutes the proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering, FASE 2013, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2013, which took place in Rome, Italy, in March 2013. The 25 papers presented in this volume were carefully reviewed and selected from 112 submissions. They are organized in topical sections named: model-driven engineering; verification and validation; software comprehension; analysis tools; model-driven engineering: applications; model transformations; and testing.

Table of Contents

Frontmatter

Invited Paper

Variability in Software: State of the Art and Future Directions
(Extended Abstract)
Abstract
Variability is a fundamental aspect of software. It is the ability to create system variants for different market segments or contexts of use. Variability has been most extensively studied in software product lines [10], but is also relevant in other areas, including software ecosystems [4] and context-aware software [15]. Virtually any successful software faces eventually the need to exist in multiple variants.
Krzysztof Czarnecki

Model-Driven Engineering: Concepts

Towards a Distributed Modeling Process Based on Composite Models
Abstract
The rising impact of software development in globally distributed teams strengthens the need for strategies that establish a clear separation of concerns in software models. Dealing with large, weakly modularized models and conflicting changes on interrelated models are typical obstacles to be witnessed. This paper proposes a structured process for distributed modeling based on the modularization technique provided by composite models with explicit interfaces. It provides a splitting activity for decomposing large models, discusses asynchronous and synchronous editing steps in relation to consistency management and provides a merge activity allowing the reuse of code generators. All main concepts of composite modeling are precisely defined based on category theory.
Daniel Strüber, Gabriele Taentzer, Stefan Jurack, Tim Schäfer
Change Propagation due to Uncertainty Change
Abstract
Uncertainty is ubiquitous in software engineering; however, it has been typically handled in adhoc and informal ways within software models. Automated change propagation is recognized as a key tool for managing the accidental complexity that comes with multiple interrelated models. In this paper, we address change propagation in the context of model uncertainty and consider the case where changes in the level of uncertainty in a model can be propagated to related models. We define such uncertainty change propagation using our earlier formalization and develop automated propagation algorithms using an SMT solver. A preliminary evaluation shows that the approach is feasible.
Rick Salay, Jan Gorzny, Marsha Chechik
A Model-Based Synthesis Process for Choreography Realizability Enforcement
Abstract
The near future in service-oriented system development envisions a ubiquitous world of available services that collaborate to fit users’ needs. Modern service-oriented applications are often built by reusing and assembling distributed services. This can be done by considering a global specification of the interactions between the participant services, namely the choreography. In this paper, we propose a synthesis approach to automatically synthesize a choreography out of a specification of it and a set of services discovered as suitable participants. The synthesis is model-based in the sense that it works by assuming a finite state model of the services’s protocol and a BPMN model for the choreography specification. The result of the synthesis is a set of distributed components, called coordination delegates, that coordinate the services’ interaction in order to realize the specified choreography. The work advances the state-of-the-art in two directions: (i) we provide a solution to the problem of choreography realizability enforcement, and (ii) we provide a model-based tool chain to support the development of choreography-based systems.
Marco Autili, Davide Di Ruscio, Amleto Di Salle, Paola Inverardi, Massimo Tivoli
On Extracting Feature Models from Sets of Valid Feature Combinations
Abstract
Rather than developing individual systems, Software Product Line Engineering develops families of systems. The members of the software family are distinguished by the features they implement and Feature Models (FMs) are the de facto standard for defining which feature combinations are considered valid members. This paper presents an algorithm to automatically extract a feature model from a set of valid feature combinations, an essential development step when companies, for instance, decide to convert their existing product variations portfolio into a Software Product Line. We performed an evaluation on 168 publicly available feature models, with 9 to 38 features and up to 147456 feature combinations. From the generated feature combinations of each of these examples, we reverse engineered an equivalent feature model with a median performance in the low milliseconds.
Evelyn Nicole Haslinger, Roberto Erick Lopez-Herrejon, Alexander Egyed

Verification and Validation 1

On the Empirical Evaluation of Fault Localization Techniques for Spreadsheets
Abstract
Spreadsheets are by far the most prominent example of end-user programs of ample size and substantial structural complexity. In addition, spreadsheets are usually not tested very rigorously and thus comprise faults. Locating faults is a hard task due to the size and the structure, which is usually not directly visible to the user, i.e., the functions are hidden behind the cells and only the computed values are presented. Hence, there is a strong need for debugging support. In this paper, we adapt three program-debugging approaches that have been designed for more traditional procedural or object-oriented programming languages. These techniques are Spectrum-based Fault Localization, Spectrum-Enhanced Dynamic Slicing, and Constraint-based Debugging. Beside the theoretical foundations, we present a more sophisticated empirical evaluation including a comparison of these approaches. The empirical evaluation shows that Sfl (Spectrum-based Fault Localization) and Sendys (Spectrum ENhanced Dynamic Slicing) are the most promising techniques.
Birgit Hofer, André Riboira, Franz Wotawa, Rui Abreu, Elisabeth Getzner
Quality of Merge-Refactorings for Product Lines
Abstract
In this paper, we consider the problem of refactoring related software products specified in UML into annotative product line representations. Our approach relies on identifying commonalities and variabilities in existing products and further merging those into product line representations which reduce duplications and facilitate reuse. Varying merge strategies can lead to producing several semantically correct, yet syntactically different refactoring results. Depending on the goal of the refactoring, one result can be preferred to another. We thus propose to capture the goal using a syntactic quality function and use that function to guide the merge strategy. We define and implement a quality-based merge-refactoring framework for UML models containing class and statechart diagrams and report on our experience applying it on three case-studies.
Julia Rubin, Marsha Chechik

Software Comprehension

Towards Understanding the Behavior of Classes Using Probabilistic Models of Program Inputs
Abstract
We propose an approach to characterize the behavior of classes using dynamic coupling distributions. To this end, we propose a general framework for modeling execution possibilities of a program by defining a probabilistic model over the inputs that drive the program. Because specifying inputs determines a particular execution, this model defines implicitly a probability distribution over the set of executions, and also over the coupling values calculated from them. Our approach is illustrated through two case studies representing two categories of programs. In the first case, the number of inputs is fixed (batch and command line programs) whereas, in the second case, the number of inputs is variable (interactive programs).
Arbi Bouchoucha, Houari Sahraoui, Pierre L’Ecuyer
Discovering Branching Conditions from Business Process Execution Logs
Abstract
Process mining is a family of techniques to discover business process models and other knowledge of business processes from event logs. Existing process mining techniques are geared towards discovering models that capture the order of execution of tasks, but not the conditions under which tasks are executed – also called branching conditions. One existing process mining technique, namely ProM’s Decision Miner, applies decision tree learning techniques to discover branching conditions composed of atoms of the form “v op c” where “v” is a variable, “op” is a comparison predicate and “c” is a constant. This paper puts forward a more general technique to discover branching conditions where the atoms are linear equations or inequalities involving multiple variables and arithmetic operators. The proposed technique combine invariant discovery techniques embodied in the Daikon system with decision tree learning techniques.
Massimiliano de Leoni, Marlon Dumas, Luciano García-Bañuelos
Exposing Behavioral Differences in Cross-Language API Mapping Relations
Abstract
Due to various considerations, software vendors often translate their applications from one programming language to another, either manually or with the support of translation tools. Both these scenarios require translation of many call sites of API elements (i.e., classes, methods, and fields of API libraries). API mapping relations, either acquired by experienced programmers or already incorporated in translation tools, are much valuable in the translation process, since they describe mapping relations between source API elements and their equivalent target API elements. However, in an API mapping relation, a source API element and its target API elements may have behavioral differences, and such differences could lead to defects in the translated code. So far, to the best of our knowledge, there exists no previous study for exposing or understanding such differences. In this paper, we make the first attempt to expose and analyze behavioral differences in cross-language API mapping relations. From our result, we summarize eight findings and their implications that can improve effectiveness of translation tools, and also assist programmers in understanding the differences between mapped API elements of different languages during the translation process. Some exposed behavioral differences can indicate defects in translation tools, and four such new defects were confirmed by the developers of those tools.
Hao Zhong, Suresh Thummalapenta, Tao Xie

Verification and Validation 2

Explicit-State Software Model Checking Based on CEGAR and Interpolation
Abstract
Abstraction, counterexample-guided refinement, and interpolation are techniques that are essential to the success of predicate-based program analysis. These techniques have not yet been applied together to explicit-value program analysis. We present an approach that integrates abstraction and interpolationbased refinement into an explicit-value analysis, i.e., a program analysis that tracks explicit values for a specified set of variables (the precision). The algorithm uses an abstract reachability graph as central data structure and a path-sensitive dynamic approach for precision adjustment. We evaluate our algorithm on the benchmark set of the Competition on Software Verification 2012 (SV-COMP’12) to show that our new approach is highly competitive. We also show that combining our new approach with an auxiliary predicate analysis scores significantly higher than the SV-COMP’12 winner.
Dirk Beyer, Stefan Löwe
Design Pattern-Based Extension of Class Hierarchies to Support Runtime Invariant Checks
Abstract
We present a technique for automatically weaving structural invariant checks into an existing collection of classes. Using variations on existing design patterns, we use a concise specification to generate from this collection a new set of classes that implement the interfaces of the originals, but with the addition of user-specified class invariant checks. Our work is notable in the scarcity of assumptions made. Unlike previous design pattern approaches to this problem, our technique requires no modification of the original source code, relies only on single inheritance, and does not require that the attributes used in the checks be publicly visible. We are able to instrument a wide variety of class hierarchies, including those with pure interfaces, abstract classes and classes with type parameters. We have implemented the construction as an Eclipse plug-in for Java development.
John Lasseter, John Cipriano
Augmenting Sequence Enumeration with String-Rewriting for Requirements Analysis and Behavioral Specification
Abstract
Sequence enumeration is a method for deriving a system model based on informal requirements. Under sequence enumeration, stimulus (input) sequences are considered in a breadth-first manner, with the expected system response to each sequence given. Not all sequences of stimuli are considered since a sequence need not be extended if either it is illegal (it cannot be applied in practice) or it can be reduced to another sequence previously considered (the sequences take the system to the same state). Sequence enumeration is mostly a manual process, which leads to a model that can be used as the basis for automation. This paper describes a method, based on string-rewriting, that automates parts of sequence enumeration. This automation has the potential to reduce both the cost and time involved in sequence enumeration but also to reduce the scope for human error. In addition to outlining this method, we discuss our experiences in applying it to four case studies.
Lan Lin, Jesse H. Poore, Robert Eschbach, Robert M. Hierons, Christopher Robinson-Mallett
Scenario Realizability with Constraint Optimization
Abstract
This work considers implementation of requirements expressed as High-level Message Sequence Charts (HMSCs). All HMSCs are not implementable, but a particular subclass called local HMSCs can be implemented using a simple projection operation. This paper proposes a new technique to transform an arbitrary HMSC specification into a local HMSC, hence allowing implementation. We show that this transformation can be automated as a constraint optimization problem. The impact of modifications brought to the original specification can be minimized w.r.t. a cost function. The approach was evaluated on a large number of randomly generated HMSCs. The results show an average runtime of a few seconds, which demonstrates applicability of the technique.
Rouwaida Abdallah, Arnaud Gotlieb, Loïc Hélouët, Claude Jard

Analysis Tools

Andromeda: Accurate and Scalable Security Analysis of Web Applications
Abstract
Security auditing of industry-scale software systems mandates automation. Static taint analysis enables deep and exhaustive tracking of suspicious data flows for detection of potential leakage and integrity violations, such as cross-site scripting (XSS), SQL injection (SQLi) and log forging. Research in this area has taken two directions: program slicing and type systems. Both of these approaches suffer from a high rate of false findings, which limits the usability of analysis tools based on these techniques. Attempts to reduce the number of false findings have resulted in analyses that are either (i) unsound, suffering from the dual problem of false negatives, or (ii) too expensive due to their high precision, thereby failing to scale to real-world applications.
In this paper, we investigate a novel approach for enabling precise yet scalable static taint analysis. The key observation informing our approach is that taint analysis is a demand-driven problem, which enables lazy computation of vulnerable information flows, instead of eagerly computing a complete data-flow solution, which is the reason for the traditional dichotomy between scalability and precision. We have implemented our approach in Andromeda, an analysis tool that computes data-flow propagations on demand, in an efficient and accurate manner, and additionally features incremental analysis capabilities. Andromeda is currently in use in a commercial product. It supports applications written in Java, .NET and JavaScript. Our extensive evaluation of Andromeda on a suite of 16 production-level benchmarks shows Andromeda to achieve high accuracy and compare favorably to a state-of-the-art tool that trades soundness for precision.
Omer Tripp, Marco Pistoia, Patrick Cousot, Radhia Cousot, Salvatore Guarnieri
VerChor: A Framework for Verifying Choreographies
Abstract
Nowadays, modern applications are often constructed by reusing and assembling distributed and collaborating entities, e.g., software components, Web services, or Software as a Service in cloud computing environments. In order to facilitate the integration of independently developed components (i.e., peers) that may reside in different organizations, it is necessary to provide a global contract to which the peers participating in a service composition should adhere. Such a contract is called choreography, and specifies interactions among a set of services from a global point of view.
Matthias Güdemann, Pascal Poizat, Gwen Salaün, Alexandre Dumont
Javanni: A Verifier for JavaScript
Abstract
JavaScript ranks among the most popular programming languages for the web, yet its highly dynamic type system and occasionally unintuitive semantics make programming particularly error-prone. This paper presents Javanni, a verifier for JavaScript programs that can statically detect many common programming errors. Javanni checks the absence of standard type-related errors (such as accessing undefined fields) without requiring user-written annotations, and it can also verify full functional-correctness specifications. Several experiments with JavaScript applications reported in the paper demonstrate that Javanni is flexibly usable on programs with non-trivial specifications. Javanni is available online within the CloudStudio web integrated environment.
Martin Nordio, Cristiano Calcagno, Carlo Alberto Furia

Model-Driven Engineering: Applications

Model-Based Implementation of Parallel Real-Time Systems
Abstract
One of the main challenges in the design of real-time systems is how to derive correct and efficient implementations from platform-independent specifications.
We present a general implementation method in which the application is represented by an abstract model consisting of a set of interacting components. The abstract model executes sequentially components interactions atomically and instantaneously. We transform abstract models into physical models representing their execution on a platform. Physical models take into account execution times of interactions and allow their parallel execution. They are obtained by breaking atomicity of interactions using a notion of partial state. We provide safety conditions guaranteeing that the semantics of abstract models is preserved by physical models. These provide bases for implementing a parallel execution engine coordinating the execution of the components. The implementation has been validated on a real robotic application. Benchmarks show net improvement of its performance compared to a sequential implementation.
Ahlem Triki, Jacques Combaz, Saddek Bensalem, Joseph Sifakis
A Grey-Box Approach for Automated GUI-Model Generation of Mobile Applications
Abstract
As the mobile platform continues to pervade all aspects of human activity, and mobile applications, or mobile apps for short, on this platform tend to be faulty just like other types of software, there is a growing need for automated testing techniques for mobile apps. Modelbased testing is a popular and important testing approach that operates on a model of an app’s behavior. However, such a model is often not available or of insufficient quality. To address this issue, we present a novel grey-box approach for automatically extracting a model of a given mobile app. In our approach, static analysis extracts the set of events supported by the Graphical User Interface (GUI) of the app. Then dynamic crawling reverse-engineers a model of the app, by systematically exercising these events on the running app. We also present a tool implementing this approach for the Android platform. Our empirical evaluation of this tool on several Android apps demonstrates that it can efficiently extract compact yet reasonably comprehensive models of high quality for such apps.
Wei Yang, Mukul R. Prasad, Tao Xie
A Mechanized Model for CAN Protocols
Abstract
Formal reasoning on Peer-to-Peer (P2P) systems is an intimidating task. This paper focuses on broadcast algorithms for Content Addressable Network (CAN). Since these algorithms run on top of complex P2P systems, finding the right level of abstraction in order to prove their functional correctness is difficult. This paper presents a mechanized model for both CAN and broadcast protocols over those networks. We demonstrate that our approach is practical by identifying sufficient conditions for a protocol to be correct and efficient. We also prove the existence of a protocol verifying those properties.
Francesco Bongiovanni, Ludovic Henrio

Model Transformations

Enforcing QVT-R with mu-Calculus and Games
Abstract
QVT-R is the standard Object Management Group bidirectional transformation language. In previous work, we gave a precise game-theoretic semantics for the checkonly semantics of QVT-R transformations, including the recursive invocation of relations which is allowed and used, but not defined, by the QVT standard. In this paper, we take up the problem of enforce semantics, where the standard attempts formality, but at crucial points lapses into English. We show that our previous semantics can be extended to enforce mode, giving a precise semantics taking the standard into account.
Julian Bradfield, Perdita Stevens
Implementing QVT-R Bidirectional Model Transformations Using Alloy
Abstract
QVT Relations (QVT-R) is the standard language proposed by the OMG to specify bidirectional model transformations. Unfortunately, in part due to ambiguities and omissions in the original semantics, acceptance and development of effective tool support has been slow. Recently, the checking semantics of QVT-R has been clarified and formalized. In this paper we propose a QVT-R tool that complies to such semantics. Unlike any other existing tool, it also supports meta-models enriched with OCL constraints (thus avoiding returning ill-formed models), and proposes an alternative enforcement semantics that works according to the simple and predictable “principle of least change”. The implementation is based on an embedding of both QVT-R transformations and UML class diagrams (annotated with OCL) in Alloy, a lightweight formal specification language with support for automatic model finding via SAT solving.
Nuno Macedo, Alcino Cunha
Abstraction and Training of Stochastic Graph Transformation Systems
Abstract
Simulation of stochastic graph transformation systems (SGTS) allows us to analyse the model’s behaviour. However, complexity of models limits our capability for analysis. In this paper, we aim to simplify models by abstraction while preserving relevant trends in their global behaviour. Based on a hierarchical graph model inspired by membrane systems, structural abstraction is achieved by “zooming out” of membranes, hiding their internal state. We use Bayesian networks representing dependencies on stochastic (input) parameters, as well as causal relationships between rules, for parameter learning and inference. We demonstrate and evaluate this process via two case studies, immunological response to a viral attack and reconfiguration in P2P networks.
Mayur Bapodra, Reiko Heckel

Testing

Discovering Math APIs by Mining Unit Tests
Abstract
In today’s API-rich world, programmer productivity depends heavily on the programmer’s ability to discover the required APIs. In this paper, we present a technique and tool, called MathFinder, to discover APIs for mathematical computations by mining unit tests of API methods. Given a math expression, MathFinder synthesizes pseudo-code to compute the expression by mapping its subexpressions to API method calls. For each subexpression, MathFinder searches for a method such that there is a mapping between method inputs and variables of the subexpression. The subexpression, when evaluated on the test inputs of the method under this mapping, should produce results that match the method output on a large number of tests. We implemented MathFinder as an Eclipse plugin for discovery of third-party Java APIs and performed a user study to evaluate its effectiveness. In the study, the use of MathFinder resulted in a 2x improvement in programmer productivity. In 96% of the subexpressions queried for in the study, MathFinder retrieved the desired API methods as the top-most result. The top-most pseudo-code snippet to implement the entire expression was correct in 93% of the cases. Since the number of methods and unit tests to mine could be large in practice, we also implement MathFinder in a MapReduce framework and evaluate its scalability and response time.
Anirudh Santhiar, Omesh Pandita, Aditya Kanade
POGen: A Test Code Generator Based on Template Variable Coverage in Gray-Box Integration Testing for Web Applications
Abstract
Web applications are complex; they consist of many subsystems and run on various browsers and platforms. This makes it difficult to conduct adequate integration testing to detect faults in the connections between subsystems or in the specific environments. Therefore, establishing an efficient integration testing method with the proper test adequacy criteria and tools is an important issue.
In this paper, we propose a new test coverage called template variable coverage. We also propose a novel technique for generating skeleton test code that includes accessor methods and improves the template variable coverage criterion, using a tool that we developed called POGen. Our experiments show that template variable coverage correlates highly with the capability to detect faults, and that POGen can reduce testing costs.
Kazunori Sakamoto, Kaizu Tomohiro, Daigo Hamura, Hironori Washizaki, Yoshiaki Fukazawa
Testing with Inputs and Outputs in CSP
Abstract
This paper addresses refinement and testing based on CSP models, when we distinguish input and output events. From a testing perspective, there is an asymmetry: the tester (or the environment) controls the inputs, and the system under test controls the outputs. The standard models and refinement relations of CSP are, therefore, not entirely suitable for testing. Here, we adapt the CSP stable-failures model, resulting in the notion of input-output failures refinement. We compare that with the ioco relation often used in testing.Finally, we adapt the CSP testing theory, and show that some tests become unnecessary.
Ana Cavalcanti, Robert M. Hierons
Backmatter
Metadata
Title
Fundamental Approaches to Software Engineering
Editors
Vittorio Cortellessa
Dániel Varró
Copyright Year
2013
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-37057-1
Print ISBN
978-3-642-37056-4
DOI
https://doi.org/10.1007/978-3-642-37057-1

Premium Partner

    Image Credits