Research Track session

Many modern user-intensive applications, such as Web applications, must satisfy the interaction requirements of thousands if not millions of users, which can be hardly fully understood at design time. Designing applications that meet user behaviors, by efficiently supporting the prevalent navigation patterns, and evolving with them requires new approaches that go beyond classic software engineering solutions. We present a novel approach that automates the acquisition of user-interaction requirements in an incremental and reflective way. Our solution builds upon inferring a set of probabilistic Markov models of the users' navigational behaviors, dynamically extracted from the interaction history given in the form of a log file. We annotate and analyze the inferred models to verify quantitative properties by means of probabilistic model checking. The paper investigates the advantages of the approach referring to a Web application currently in use.

Most application code evolves incrementally, and especially so when being maintained after the applications have been deployed. Yet, most data-flow analyses do not take advantage of this fact. Instead they require clients to recompute the entire analysis even if little code has changed—a time consuming undertaking, especially with large libraries or when running static analyses often, e.g., on a continuous-integration server. In this work, we present Reviser, a novel approach for automatically and efficiently updating inter-procedural dataflow analysis results in response to incremental program changes. Reviser follows a clear-and-propagate philosophy, aiming at clearing and recomputing analysis information only where required, thereby greatly reducing the required computational effort. The Reviser algorithm is formulated as an extension to the IDE framework for Inter-procedural Finite Distributed Environment problems and automatically updates arbitrary IDE-based analyses. We have implemented Reviser as an open-source extension to the Heros IFDS/IDE solver and the Soot program-analysis framework. An evaluation of Reviser on various client analyses and target programs shows performance gains of up to 80% in comparison to a full recomputation. The experiments also show Reviser to compute the same results as a full recomputation on all instances tested.

Self-adaptation enables software to execute successfully in dynamic, unpredictable, and uncertain environments. Control theory provides a broad set of mathematically grounded techniques for adapting the behavior of dynamic systems. While it has been applied to specific software control problems, it has proved difficult to define methodologies allowing non-experts to systematically apply control techniques to create adaptive software. These difficulties arise because computer systems are usually non-linear, with varying workloads and heterogeneous components, making it difficult to model software as a dynamic system; i.e., by means of differential or difference equations. This paper proposes a broad scope methodology for automatically constructing both an approximate dynamic model of a software system and a suitable controller for managing its non-functional requirements. Despite its generality, this methodology provides formal guarantees concerning the system's dynamic behavior by keeping its model continuously updated to compensate for changes in the execution environment and effects of the initial approximation. We apply the methodology to three case studies, demonstrating its generality by tackling different domains (and different non-functional requirements) with the same approach. Being broadly applicable and fully automated, this methodology may allow the adoption of control theoretical solutions (and their formal properties) for a wide range of software adaptation problems.

Probabilistic model checking is a quantitative verification technology for computer systems and has been the focus of intense research for over a decade. While in many circumstances of probabilistic model checking it is reasonable to anticipate a possible discrepancy between a stochastic model and a real-world system it represents, the state-of-the-art provides little account for the effects of this discrepancy on verification results. To address this problem, we present a perturbation approach in which quantities such as transition probabilities in the stochastic model are allowed to be perturbed from their measured values. We present a rigorous mathematical characterization for variations that can occur to verification results in the presence of model perturbations. The formal treatment is based on the analysis of a parametric variant of discrete-time Markov chains, called parametric Markov chains (PMCs), which are equipped with a metric to measure their perturbed vector variables. We employ an asymptotic method from perturbation theory to compute two forms of perturbation bounds, namely condition numbers and quadratic bounds, for automata-based verification of PMCs. We also evaluate our approach with case studies on variant models for three widely studied systems, the Zeroconf protocol, the Leader Election Protocol and the NAND Multiplexer.