IEEE Transactions on Software Engineering

PrePrint: Loupe: Verifying Publish-Subscribe Architectures with a Magnifying Lens

The Publish-Subscribe (P/S) paradigm fosters decoupling among distributed components. This facilitates designing of dynamic applications, but also impacts negatively on their verification. In addition, existing P/S infrastructures offer different features to the applications, e.g., in terms of message reliability. This complicates the verification, as its outcome depends on the guarantees provided by the underlying P/S system. Although model checking has been proposed for the verification of P/S architectures, existing solutions overlook many characteristics of the communication infrastructure to avoid state explosion problems. To overcome these limitations, the Loupe domain-specific model checker adopts a different approach. The P/S infrastructure is not modeled on top of a general-purpose model checker. Instead, it is embedded within the checking engine, and the traditional P/S operations become part of the modeling language. In this article, we describe Loupe's design and the state abstractions that enable accurate verification without incurring in state explosion problems. We illustrate our use of state-of-the-art software verification tools to assess some key functionality in Loupe. A complete case study shows how Loupe eases the verification of P/S architectures. Finally, we quantitatively compare Loupe's performance against alternative approaches. The results indicate that Loupe is effective and efficient in enabling accurate verification of P/S architectures.

PrePrint: Automatically Detecting and Tracking Inconsistencies in Software Design Models

Software models typically contain many inconsistencies and consistency checkers help engineers find them. Even if engineers are willing to tolerate inconsistencies, they are better off knowing about their existence to avoid follow-on errors and unnecessary rework. However, current approaches do not detect or track inconsistencies fast enough. This paper presents an automated approach for detecting and tracking inconsistencies in real time (while the model changes). Engineers only need to define consistency rules - in any language - and our approach automatically identifies how model changes affect these consistency rules. It does this by observing the behavior of consistency rules to understand how they affect the model. The approach is quick, correct, scalable, fully automated, and easy to use as it does not require any special skills from the engineers using it. We evaluated the approach on 34 models with model sizes of up to 162,237 model elements and 24 types of consistency rules. Our empirical evaluation shows that our approach requires only 1.4 ms to re-evaluate the consistency of the model after a change (in average), its performance is not noticeably affected by the model size and common consistency rules but only by the number of consistency rules, at the expense of a quite acceptable, linearly increasing memory consumption.

PrePrint: Self-supervising BPEL Processes

Service compositions suffer changes in their partner services. Even if the composition does not change, its behavior may evolve over time and become incorrect. Such changes cannot be fully foreseen through pre-release validation, but impose a shift in the quality assessment activities. Provided functionality and quality of service must be continuously probed while the application executes, and the application itself must be able to take corrective actions to preserve its dependability and robustness. We propose the idea of self-supervising BPEL processes, that is, special-purpose compositions that assess their behavior and react through user-defined rules. Supervision consists of monitoring and recovery. The former checks the system's execution to see whether everything is proceeding as planned, while the latter attempts to fix any anomalies. The article introduces two languages for defining monitoring and recovery and explains how to use them to enrich BPEL processes with self-supervision capabilities. Supervision is treated as a cross-cutting concern that is only blended at runtime, allowing different stakeholders to adopt different strategies with no impact on the actual business logic. The paper also presents a supervision-aware run-time framework for executing the enriched processes, and briefly discusses the results of in-lab experiments and of a first evaluation with industrial partners.

PrePrint: Verification and Trade-off Analysis of Security Properties in UML System Models

Designing secure systems is a non-trivial task. Incomplete or faulty designs can cause security mechanisms to be incorrectly incorporated in a system, allowing them to be by-passed and resulting in a security breach. We advocate the use of the Aspect-Oriented Risk-Driven Development (AORDD) methodology for developing secure systems. This methodology begins with designers defining system assets, identifying potential attacks against them, and evaluating system risks. When a risk is unacceptable, designers must mitigate the associated threat by incorporating security mechanisms methodically into the system design. Designers formally evaluate the resulting design to ensure the threat has been mitigated, while still allowing development to meet other project constraints. In this paper, we focus on the AORDD analysis, which consists of: 1) a formal security evaluation, and 2) a trade-off analysis that enables system designers to position alternative security solutions against each other. The formal security evaluation uses the Alloy Analyzer to provide assurance that an incorporated security mechanism performs as expected and makes the system resilient to previously identified attacks. The trade-off analysis uses a Bayesian Belief Network topology to allow equally effective security mechanisms to be compared against system security requirements and other factors such as time-to-market and budget constraints.

PrePrint: Context-Aware Adaptive Applications: Fault Patterns and Their Automated Identification

Applications running on mobile devices are intensely context-aware and adaptive. Streams of context values continuously drive these applications, making them very powerful but at the same time susceptible to undesired configurations. Such configurations are not easily exposed by existing validation techniques, thereby leading to new analysis and testing challenges. In this paper we address some of these challenges by defining and applying a new model of adaptive behavior called an A-FSM to enable the detection of faults caused by both erroneous adaptation logic and asynchronous updating of context information, with the latter leading to inconsistencies between the external physical context and its internal representation within an application. We identify a number of adaptation fault patterns, each describing a class of faulty behaviors. Finally, we describe three classes of algorithms to detect such faults automatically via analysis of the A-FSM. We evaluate our approach and the tradeoffs between the classes of algorithms on a set of synthetically generated CAAAs and on a simple but realistic application in which a cellphone's configuration profile changes automatically as a result of changes to the user's location, speed and surrounding environment. Our evaluation describes the faults our algorithms are able to detect and compares the algorithms in terms of their performance and storage requirements.

PrePrint: Interactive, Evolutionary Search in Upstream Object-oriented Class Design

Although much evidence exists to suggest that early lifecycle software engineering design is a difficult task for software engineers to perform, current computational tool support for software engineers is limited. To address this limitation, interactive search-based approaches using evolutionary computation and software agents are investigated in experimental upstream design episodes for two example design domains. Results show that interactive evolutionary search, supported by software agents, appears highly promising. As an open system, search is steered jointly by designer preferences and software agents. Directly traceable to the design problem domain, a mass of useful and interesting class designs is arrived at which may be visualized by the designer with quantitative measures of structural integrity such as design coupling and class cohesion. The class designs are found to be of equivalent or better coupling and cohesion when compared to a manual class design for the example design domains, and by exploiting concurrent execution, the run-time performance of the software agents is highly favorable.

PrePrint: Systematic Review and Aggregation of Empirical Studies on Elicitation Techniques

We have located the results of empirical studies on elicitation techniques and aggregated these results to gather empirically grounded evidence. Our chosen surveying methodology was systematic review, whereas we used an adapta-tion of comparative analysis for aggregation because metaanalysis techniques could not be applied. The review identified 564 publications from the SCOPUS, IEEEXPLORE and ACM DL databases, as well as Google. We selected and extracted data from 26 of those publications. The selected publications contain 30 empirical studies. These studies were designed to test 43 elicitation techniques and 50 different response variables. We got a hundred separate results from the experiments. The aggregation generated 17 pieces of knowledge about the interviewing, laddering, sorting and protocol analysis elicitation techniques. We provide a set of guidelines based on the gathered pieces of knowledge.

PrePrint: Assessing, Comparing, and Combining State Machine-Based Testing and Structural Testing: A Series of Experiments

A large number of research works have addressed the importance of models in software engineering. However, the adoption of model-based techniques in software organizations is limited since these models are perceived to be expensive and not necessarily cost-effective. Focusing on model-based testing, this paper reports on a series of controlled experiments. It investigates the impact of state machine testing on fault detection in class clusters and its cost when compared with structural testing. Based on previous work showing this is a good compromise in terms of cost and effectiveness, this paper focuses on a specific state-based technique: the round-trip paths coverage criterion. Round-trip paths testing is compared to structural testing, and it is investigated whether they are complementary. Results show that, even when a state machine models as accurately as possible the behavior of the cluster under test, no significant difference between the fault detection effectiveness of the two test strategies is observed, while the two test strategies are significantly more effective when combined by augmenting state machine testing with structural testing. A qualitative analysis also investigates the reasons why test techniques do not detect certain faults and how the cost of state machine testing can be brought down.

PrePrint: Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit State Model Checking

Web script crashes and malformed dynamically-generated web pages are common errors, and they seriously impact the usability of web applications. Current tools for web-page validation cannot handle the dynamically generated pages that are ubiquitous on today’s Internet. We present a dynamic test generation technique for the domain of dynamic web applications. The technique utilizes both combined concrete and symbolic execution and explicit-state model checking. The technique generates tests automatically, runs the tests capturing logical constraints on inputs, and minimizes the conditions on the inputs to failing tests, so that the resulting bug reports are small and useful in finding and fixing the underlying faults. Our tool Apollo implements the technique for the PHP programming language. Apollo generates test inputs for a web application, monitors the application for crashes, and validates that the output conforms to the HTML specification. This paper presents Apollo's algorithms and implementation, and an experimental evaluation that revealed 673 faults in 6 PHP web applications.

PrePrint: Incremental Test Generation for Software Product Lines

The recent advances in mechanical techniques for systematic testing have increased our ability to automatically find subtle bugs, and hence to deploy more dependable software. This paper builds on one such systematic technique, scope-bounded testing, to develop a novel specification-based approach for efficiently generating tests for products in a software product line. Given properties of features as first-order logic formulas in Alloy, our approach uses SAT-based analysis to automatically generate test inputs for each product in a product line. To ensure soundness of generation, we introduce an automatic technique for mapping a formula that specifies a feature into a transformation that defines incremental refinement of test suites. Our experimental results using different data structure product lines show that an incremental approach can provide an order of magnitude speed-up over conventional techniques. We also present a further optimization using dedicated integer constraint solvers for feature properties that introduce integer constraints, and show how to use a combination of solvers in tandem for solving Alloy formulas.

PrePrint: How Reliable Are Systematic Reviews in Empirical Software Engineering?

BACKGROUND - the systematic review is becoming a more commonly employed research instrument in empirical software engineering. Before undue reliance is placed on the outcomes of such reviews it would seem useful to consider the robustness of the approach in this particular research context. OBJECTIVE - the aim of this study is to assess the reliability of systematic reviews as a research instrument. In particular we wish to investigate the consistency of process and the stability of outcomes. METHOD - we compare the results of two independent reviews under taken with a common research question. RESULTS - the two reviews find similar answers to the research question, although the means of arriving at those answers vary. CONCLUSIONS - in addressing a well-bounded research question, groups of researchers with similar domain experience can arrive at the same review outcomes, even though they may do so in different ways. This provides evidence that, in this context at least, the systematic review is a robust research method.

PrePrint: Bristlecone: Language Support for Robust Software Applications

We present Bristlecone, a programming language for robust software systems. Bristlecone applications have two components: a high-level organization specification that describes how the application's conceptual operations interact, and a low-level operational specification that describes the sequence of instructions that comprise an individual conceptual operation. Bristlecone uses the high-level organization specification to recover the software system from an error to a consistent state and to reason how to safely continue the software system's execution after the error. We have implemented a compiler for Bristlecone. We have evaluated this implementation on three benchmark applications: a web crawler, a web server, and a multi-room chat server. We developed both a Bristlecone version and a Java version of each benchmark application. We used injected failures to evaluate the robustness of each version of the application. We found that the Bristlecone versions of the benchmark applications more successfully survived the injected failures. The Bristlecone compiler contains a static analysis that operates on the organization specification to generate a set of diagrams that graphically present the task interactions in the application. We have used the analysis to help understand the high-level structure of three Bristlecone applications: a game server, a web server, and a chat server.

PrePrint: Software Module Clustering as a Multi-Objective Search Problem

Software module clustering is the problem of automatically organising software units into modules to improve program structure. There has been a great deal of recent interest in search based formulations of this problem, in which module boundaries are identified by automated search, guided by a fitness function that captures the twin objectives of high cohesion and low coupling in a single objective fitness function. This paper introduces two novel multi-objective formulations of the software module clustering problem, in which several different objectives (including cohesion and coupling) are represented separately. In order to evaluate the effectiveness of the multi-objective approach, a set of experiments were performed on 17 real-world module clustering problems. The results of this empirical study provide strong evidence to support the claim that the multi-objective approach produces significantly better solutions than the existing single-objective approach.

PrePrint: Aspect-oriented Race Detection in Java

In the past researchers have developed specialized programs to aid programmers detecting concurrent programming errors such as deadlocks, livelocks, starvation and data races. In this work we propose a language extension to the aspect-oriented programming language AspectJ, in the form of three new pointcuts, lock(), unlock() and maybeShared(). These pointcuts allow programmers to monitor program events where locks are granted or handed back, and where values are accessed that may be shared amongst multiple Java threads. We decide thread-locality using a static thread-local-objects analysis developed by others. Using the three new primitive pointcuts, researchers can directly implement efficient monitoring algorithms to detect concurrent-programming errors online. As an example, we describe a new algorithm which we call Racer, an adaption of the well-known Eraser algorithm to the memory model of Java. We implemented the new pointcuts as an extension to the AspectBench Compiler, implemented the Racer algorithm using this language extension and then applied the algorithm to the NASA K9 Rover Executive and two smaller programs. Our experiments proved our implementation very effective. In the Rover Executive Racer finds 12 data races, with no false warnings. Only one of these races was previously known.

PrePrint: Efficient Software Verification: Statistical Testing Using Automated Search

Statistical testing has been shown to be more efficient at detecting faults in software than other methods of dynamic testing such as random and structural testing. Test data is generated by sampling from a probability distribution chosen so that each element of the software's structure is exercised with a high probability. However, deriving a suitable distribution is difficult for all but the simplest of programs. This paper demonstrates that automated search is a practical method of finding near-optimal probability distributions for real-world programs, and that test sets generated from these distributions continue to show superior efficiency in detecting faults in the software.

PrePrint: Semi-Proving: An Integrated Method for Program Proving, Testing, and Debugging

We present an integrated method for program proving, testing, and debugging. Using the concept of metamorphic relations, we select necessary properties for target programs. For programs where global symbolic evaluation can be conducted and the constraint expressions involved can be solved, we can either prove that these necessary conditions for program correctness are satisfied, or identify all inputs that violate the conditions. For other programs, our method can be converted into a symbolic testing approach. Our method extrapolates from the correctness of a program for tested inputs to the correctness of the program for related untested inputs. The method supports automatic debugging through the identification of constraint expressions that reveal failures.

PrePrint: Plat_Forms: A Web Development Platform Comparison by an Exploratory Experiment Searching for Emergent Platform Properties

Background: For developing web-based applications, there exist several competing and widely used technological platforms (consisting of a programming language, framework(s), components, and tools), each with an accompanying development culture and style. Research question: Do web development projects exhibit emergent process or product properties that are characteristic and consistent within a platform but show relevant substantial differences across platforms or do team-to-team individual differences outweigh such differences, if any? Such a property could be positive (i.e. a platform advantage), negative, or neutral and it might be unobvious which is which. Method: In a non-randomized, controlled experiment (quasi-experiment), framed as a public contest called "Plat_Forms", top-class teams of three professional programmers competed to implement the same requirements for a web-based application within 30 hours. Three different platforms (Java EE, PHP, or Perl) were used by three teams each. We compare the resulting nine products and process records along many dimensions, both external (usability, functionality, reliability, security, etc.) and internal (size, structure, modifiability, etc.). Results: The various results obtained cover a wide spectrum: First, there are results that many people would have called "obvious" or "well known", say, that Perl solutions tend to be more compact than Java solutions. Second, there

PrePrint: Deriving a Slicing Algorithm via FermaT Transformations

In this paper we present a case study in deriving an algorithm from a formal specification via FermaT transformations. The general method (which is presented in a separate paper) is extended to a method for deriving an implementation of a program transformation from a specification of the program transformation. We use program slicing as an example transformation, since this is of interest outside the program transformation community. We develop a formal specification for program slicing, in the form of a WSL specification statement, which is refined into a simple slicing algorithm by applying a sequence of general purpose program transformations and refinements. Finally, we show how the same methods can be used to derive an algorithm for semantic slicing. The main novel contributions of this paper are: (1) Developing a formal specification for slicing. (2) Expressing the definition of slicing in terms of a WSL specification statement. (3) By applying correctness preserving transformations to the specification we can derive a simple slicing algorithm.

PrePrint: Developing a Single Model and Test Prioritization Strategies for Event-Driven Software

Event-Driven Software (EDS) is a popular type of software that can change state based on incoming events. These applications pose a challenge to testing because there are a large number of possible event sequences that users can invoke through a user interface. This work provides the first single model that is generic enough to study two types of EDS together, that of stand-alone GUI and web-based applications. As a first step, in this paper, we use the model to define generic prioritization criteria that are applicable to both GUI and web applications. Our ultimate goal is to evolve the model and use it to develop a unified theory of how all EDS should be tested. An empirical study reveals that the GUI- and web-based applications, when recast using the new model, show similar behavior. For example, a criterion that gives high priority to testing all pairs of event interactions did well for GUI as well as web applications; another criterion that gives high priority to testing the smallest number of parameter value settings did poorly for both subclasses. These results reinforce our belief that these two subclasses of applications should be modeled and studied together; other results which indicated dissimilar behavior have created opportunities for model evolution and future experimentation.

PrePrint: A Framework for Programming Robust Context-Aware Applications

In this paper we present a forward recovery model for programming robust context-aware applications. The mechanisms devised as part of this model fall into two categories: asynchronous event handling and synchronous exception handling. These mechanisms enable designing of various kinds of recovery actions to handle different kinds of failure conditions arising in context-aware applications. These include, service discovery failures, service binding failures, exceptions raised by a service, and context invalidations. The salient feature of the forward recovery model is the juxtaposition of system-level recovery with human-centric recovery for designing robust context-aware applications. This model is integrated in the high-level programming framework that we have designed for building context-aware collaborative (CSCW) applications. In this paper we demonstrate the capabilities of this model for programming various kinds of recovery patterns in context-aware applications.

PrePrint: From UML to Petri Nets: the PCM-Based Methodology

The main goal of SPE is to estimate the performance of a software before it is implemented, also comparing different design choices in order to reduce costs and time. In this paper, we present a methodology to validate the performance of a UML model, representing a software architecture. The proposed approach is based on open and well-known standards: UML for software modeling and the OMG Profile for Schedulability, Performance, and Time Specification for the performance annotations that allow to specify performance requirements into the UML model. Such specifications are collected in an intermediate model, called Performance Context Model (PCM). The intermediate model is translated into a performance model subsequently evaluated. The results obtained are fed back into the UML model. The paper is focused on the mapping from the PCM to the performance domain. More specifically, we adopt Petri nets as performance domain, specifying a mapping process based on a compositional approach we have entirely implemented into the ArgoPerformance tool. All the rules to derive a Petri net from a PCM and the performance measures assessable from the former are carefully detailed. To validate the proposed technique we provide an in depth analysis of a web application for music streaming.

PrePrint: A Quantitative Investigation of the Acceptable Risk Levels of Object-Oriented Metrics in Open-Source Systems

Object-oriented metrics have been validated empirically as measures of design complexity. These metrics can be used to mitigate potential problems in the software complexity. However, there are few studies that are conducted to formulate the guidelines, represented as threshold values, to interpret the complexity of the software design using metrics. Classes can be clustered into law and high risk groups using threshold values. In this paper, we use a statistical model, derived from the logistic regression, to identify threshold values for Chidamber and Kemerer (CK) metrics. The methodology is investigated and validated empirically on a large open-source system—the Eclipse project (Version 2.0). The empirical results indicate that the CK metrics have threshold effects at various risk levels. We have validated the use of these thresholds on the next release of the Eclipse project—Version 2.1—using decision trees. In addition, the selected threshold values were more accurate than those were selected based upon either an intuitive perspectives or data distribution parameters. Furthermore, the proposed model can be exploited to find the risk level for an arbitrary threshold value. These findings suggest that there is a relationship between risk levels and object-oriented metrics, and that, risk levels can be used to identify threshold effects.

PrePrint: Exception Handling for Repair in Service-Based Processes

This paper proposes a self-healing approach to handle exceptions in service-based processes and to repair the faulty activities with a model-based approach. In particular, a set of repair actions is defined in the process model, and repairability of the process is assessed by analyzing the process structure and the available repair actions. During execution, when an exception arises, repair plans are generated by taking into account constraints posed by the process structure, dependencies among data and available repair actions. The paper also describes the main features of the prototype developed to validate the proposed repair approach for composed Web services; the self-healing architecture for repair handling and the experimental results are illustrated. revision of manuscript submitted to: Special Issue EXCEPTION HANDLING: FROM REQUIREMENTS TO SOFTWARE MAINTENANCE

PrePrint: Understanding Exception Handling: Viewpoints of Novices and Experts

Several recent studies indicate that many industrial applications exhibit poor quality in the design of exception handling. To improve the quality of error handling we need to understand the problems and obstacles that developers face when designing and implementing exception handling. In this paper, we present our research on understanding the viewpoints of developers—novices and experts’towards exception handling. First, we conducted a study with novice developers in industry. The study results reveal that novices tend to ignore exceptions because of the complex nature of exception handling. Then, we conducted a second study with experts in industry to understand their perspective on exception handling. The study results show that for experts, exception handling is a crucial part in the development process. Experts also confirm the novices’ approach of ignoring exception handling and provide insights as to why novices do so. After analyzing the study data, we identified factors that influence experts’ strategy-selection process for handling exceptions, and then built a model that represents a strategy-selection process experts use to handle exceptions. Our model is based on interacting modules and fault scope. We conclude with some recommendations to help novices improve their understanding of exception handling.

PrePrint: Software Reliability and Testing Time Allocation: An Architecture-Based Approach

With software systems increasingly being employed in critical contexts, assuring high reliability levels for large, complex systems can incur huge verification costs. Existing standards usually assign predefined risk levels to components in the design phase, to provide some guidelines for the verification. It is a rough-grained assignment that does not consider the costs and does not provide sufficient modelling basis to let engineers quantitatively optimize resources usage. Software reliability allocation models partially address such issues, but they usually make so many assumptions on the input parameters that their application is difficult in practice. In this paper we try to reduce this gap, proposing a reliability and testing resources allocation model that is able to provide solutions at various levels of detail, depending upon the information the engineer has about the system. The model aims to quantitatively identify the most critical components of software architecture in order to best assign the testing resources to them. A tool for the solution of the model is also developed. The model is applied to an empirical case study, a program developed for the European Space Agency, to verify model's prediction abilities and evaluate the impact of the parameter estimation errors on the prediction accuracy.

PrePrint: A Genetic Algorithm-Based Stress Test Requirements Generator Tool and its Empirical Evaluation

Genetic algorithms (GAs) have been applied previously to UML-driven, stress test requirements generation with the aim of increasing chances of discovering faults relating to network traffic in distributed real-time systems. However, since evolutionary algorithms are heuristic, their performance can vary across multiple executions, which may affect robustness and scalability. To address this, we present the design and technical detail of a UML-driven, GA-based stress test requirements generation tool, together with its empirical analysis. The main goal is to analyze and improve the applicability, efficiency and effectiveness and also to validate the design choices of the GA used in the tool. Findings of the empirical evaluation reveal that the tool is robust and reasonably scalable when it is executed on large-scale experimental design models. The study also reveals the main bottlenecks and limitations of the tools, e.g., there is a performance bottleneck when the system under test has a large number of sequence diagrams which could be triggered independently from each other. In addition, issues specific to stress testing, e.g., the impact of variations in task arrival pattern types, reveal that the tool generally generates effective test requirements although the features of those test requirements might be different in different runs.

PrePrint: Time and Probability Based Information Flow Analysis

In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information flow analysis were performed by abstracting away from time and probability. It is already known that systems that are proved to be secure in a possibilistic framework may turn out to be insecure when time or probability are considered. Recently, work has been done in order to consider also aspects either of time or of probability, but not both. In this paper we propose a general framework, based on Probabilistic Timed Automata, where both probabilistic and timing covert channels can be studied. We define a Non-Interference security property and a Non Deducibility on Composition security property, which allow expressing information flow in a timed and probabilistic setting. We then compare these properties with analogous ones defined in contexts where either time or probability or neither of them are taken into account. This permits a classification of the properties depending on their discerning power. As an application, we study a system with covert channels that we are able to discover by applying our techniques.

PrePrint: Program Behavior Discovery and Verification: A Graph Grammar Approach

Discovering program behaviors and functionalities can ease program comprehension and verification. Existing program analysis approaches have used text mining algorithms to infer behavior patterns or formal models from program execution. When one tries to identify the hierarchical composition of a program behavior at different abstraction levels, textual descriptions are not informative and expressive enough. To address this, we present a semi-automatic graph grammar approach to retrieving the hierarchical structure of the program behavior. The hierarchical structure is built on recurring substructures in a bottom-up fashion. We formulate the behavior discovery and verification problem as a graph grammar induction and parsing problem, i.e. automatically iteratively mining qualified patterns and then constructing graph rewriting rules. Furthermore, using the induced grammar to parse the behavioral structure of a new program could verify if the program has the same behavioral properties specified by the grammar.

PrePrint: Assessing Software Service Quality and Trustworthiness at Selection Time

The integration of external software in project development is challenging and risky notably because the execution quality of the software and the trustworthiness of the software provider may be unknown at integration time. This is a timely problem and of increasing importance with the advent of the SaaS model of service delivery. Therefore, in choosing the SaaS service to utilize, project managers must identify and evaluate the level of risk associated with each candidate. Trust is commonly assessed through reputation systems, however existing systems rely on ratings provided by consumers. This raises numerous issues involving the subjectivity and unfairness of the service ratings. This paper describes a framework for reputation-aware software service selection and rating. A selection algorithm is devised for service recommendation, providing SaaS consumers with best possible choices based on quality, cost, and trust. An automated rating model, based on the expectancy-disconfirmation theory from market science, is also defined to overcome feedback subjectivity issues. The proposed rating and selection models are validated through simulations, demonstrating that the system can effectively capture service behaviour and recommend the best possible choices.

PrePrint: Exception Handling Patterns for Process Modeling

Process modeling allows for analysis and improvement of processes that coordinate multiple people and tools working together to carry out a task. Process modeling typically focuses on the normative process, that is, how the collaboration transpires when everything goes as desired. Unfortunately, real world processes rarely proceed that smoothly. A more complete analysis of a process requires that the process model also include details about what to do when exceptional situations arise. We have found that in many cases, there are abstract patterns that capture the relationship between exception handling tasks and the normative process. We believe process patterns can facilitate the development, documentation and maintenance of process models. In this paper, we focus on the exception handling patterns that we have observed over many years of process modeling. We describe these patterns using three process modeling notations: UML 2.0 Activity Diagrams, BPMN and Little-JIL. We present both the abstract structure of the pattern as well as examples of the pattern in use. We also provide some preliminary statistical survey data to support the claim that these patterns are found commonly in actual use and discuss the relative merits of the three notations with respect to their ability to represent these patterns.

PrePrint: Evaluation of Accuracy in Design Pattern Occurrence Detection

Detection of design pattern occurrences is part of several solutions to software engineering problems, and high accuracy of detection is important to help solve the actual problems. The improvement in accuracy of design pattern occurrence detection requires some way of evaluating various approaches. Currently, there are several different methods used in the community to evaluate accuracy. We show that these differences may greatly influence the accuracy results, which makes it nearly impossible to compare the quality of different techniques. We propose a benchmark suite to improve the situation and a community effort to contribute to, and evolve, the benchmark suite. Also, we propose fine-grained metrics assessing the accuracy of various approaches in the benchmark suite. This allows comparing the detection techniques and helps improving the accuracy of detecting design pattern occurrences.

PrePrint: Vulnerability Discovery with Attack Injection

The increasing reliance put on networked computer systems demands for higher levels of dependability. This is even more relevant as new threats and forms of attack are constantly being revealed, compromising the security of systems. The paper addresses this problem by presenting an attack injection methodology for the automatic discovery of vulnerabilities in software components. The proposed methodology, implemented in AJECT, follows an approach similar to hackers and security analysts to discover vulnerabilities in network connected servers. AJECT uses a specification of the server's communication protocol and predefined test case generation algorithms to automatically create a large number of attacks. Then, while it injects these attacks through the network, it monitors the execution of the server in the target system and the responses returned to the clients. The observation of an unexpected behavior suggests the presence of a vulnerability that was triggered by some particular attack (or group of attacks). This attack can then be used to reproduce the anomaly and to assist the removal of the error. To assess the usefulness of this approach, several attack injection campaigns were performed with 16 publicly available POP and IMAP servers. The results show that AJECT could effectively be used to locate vulnerabilities, even on well-known servers tested throughout the years.

PrePrint: On Event-Based Middleware for Location-Aware Mobile Applications

As mobile applications become more widespread, programming paradigms and middleware architectures designed to support their development are becoming increasingly important. The event-based programming paradigm is a strong candidate for the development of mobile applications due its inherent support for the loose coupling between components required by mobile applications. However, existing middleware that supports the event-based programming paradigm is not well suited to supporting location-aware mobile applications in which highly-mobile components come together dynamically to collaborate at some location. This article presents a number of techniques including location-independent announcement and subscription coupled with location-dependent filtering and event delivery that can be used by event-based middleware to support such collaboration. We describe how these techniques have been implemented in STEAM, an event-based middleware with a fully decentralized architecture, which is particularly well suited to deployment in ad hoc network environments. The cost of such location-based event dissemination and the benefits of distributed event filtering are evaluated.

PrePrint: Learning Communicating Automata from MSCs

This paper is concerned with bridging the gap between requirements and distributed systems. Requirements are defined as basic message sequence charts (MSCs) specifying positive and negative scenarios. Communicating finite-state machines (CFMs), i.e., finite automata that communicate via FIFO buffers, act as system realizations. The key contribution is a generalization of Angluin's learning algorithm for synthesizing CFMs from MSCs. This approach is exact—the resulting CFM precisely accepts the set of positive scenarions and rejects all negative ones—and yields fully asynchronous implementations. The paper investigates for which classes of MSC languages CFMs can be learned, presents an optimization technique for learning partial orders, and provides substantial empirical evidence indicating the practical feasibility of the approach.

PrePrint: Discovering Services During Service-Based System Design Using UML

Recently, there has been a proliferation of service-based systems, i.e. software systems that are composed of autonomous services, but can also use software code. In order to support the development of these systems, it is necessary to have new methods, processes, and tools. In this paper we describe a UML-based framework to assist with the development of service-based systems. The framework adopts an iterative process in which software services that can provide functional and non-functional characteristics of a system being developed are discovered, and the identified services are used to re-formulate the design models of the system. The framework uses a query language to represent structural, behavioural, and quality characteristics of services to de identified, and a query processor to match the queries against service registries. The matching process is based on distance measurements between the queries and service specfications. A prototype tool has been implemented. The work has been evaluated in terms of recall, precision, and performance measurements.

PrePrint: The Probabilistic Program Dependence Graph and Its Application to Fault Diagnosis

This paper presents an innovative model of a program's internal behavior over a set of test inputs, called the probabilistic program dependence graph (PPDG), that facilitates probabilistic analysis and reasoning about uncertain program behavior, particularly that associated with faults. The PPDG construction augments the structural dependences represented by a program dependence graph with estimates of statistical dependences between node states, which are computed from the test set. The PPDG is based on the established framework of probabilistic graphical models, which are used widely in a variety of applications. This paper presents algorithms for constructing PPDGs and applying them to fault diagnosis. This paper also presents preliminary evidence indicating that a PPDG-based fault localization technique compares favorably with existing techniques. The paper also presents evidence indicating that PPDGs can be useful for fault comprehension.

PrePrint: A Comparison of Six UML-Based Languages for Software Process Modeling

Describing and managing activities, resources and constraints of software development processes is a challenging goal for many organizations. A first generation of Software Process Modeling Languages (SPMLs) has appeared in the nineties but failed to gain broad industrial support. Recently however, a second generation of SPMLs appeared, leveraging the strong industrial interest for modeling languages such as the UML. In this article, we propose a comparison of these UML-based SPMLs. While not exhaustive, this comparison concentrates on SPMLs most representative of the various alternative approaches, ranging from UML-based framework specializations to full-blown executable meta-modeling approaches. To support the comparison of these various approaches, we propose a frame gathering a set of requirements for process modeling, such as semantic richness, modularity, executability, conformity to the UML standard, and formality. Beyond discussing the relative merits of these approaches, we also evaluate the overall suitability of these UML based SPMLs for software process modeling. Finally, we discuss the impact of these approaches on the current state of the practice, and conclude with lessons we have learned in doing this comparison.

PrePrint: A Theoretical and Empirical Study of Search-Based Testing: Local, Global and Hybrid Search

Search based optimization techniques have been applied to structural software test data generation since 1992, with a recent upsurge in interest and activity within this area. However, despite the large number of recent studies of applicability of different search based optimization approaches, there has been very little theoretical analysis of the types of testing problem for which these techniques are well-suited. There are also few empirical studies that present results for larger programs. This paper presents a theoretical exploration of the most widely studied approach, the global search technique embodied by Genetic Algorithms. It also presents results from a large empirical study that compare the behaviour of both global and local search based optimization on real world programs. The results of this study reveal that there exist cases of test data generation problems that suit each algorithm, thereby suggesting that a hybrid global-local search (a Memetic Algorithm) may be appropriate. The paper presents a Memetic Algorithm along with further empirical results studying its performance.

PrePrint: Learning a Metric for Code Readability

In this paper, we explore the concept of code readability and investigate its relation to software quality. With data collected from 120 human annotators, we derive associations between a simple set of local code features and human notions of readability. Using those features, we construct an automated readability measure and show that it can be 80% effective, and better than a human on average, at predicting readability judgments. Furthermore, we show that this metric correlates strongly with three measures of software quality: code changes, automated defect reports, and defect log messages. We measure these correlations on over 2.2 million lines of code, as well as longitudinally, over many releases of select projects. Finally, we discuss the implications of this study on programming language design and engineering practice. For example, our data suggests that comments, in of themselves, are less important than simple blank lines to local judgments of readability.

PrePrint: Engineering a Sound Assertion Semantics for the Verifying Compiler

The Verifying Compiler (VC) project is a core component of the Dependable Systems Evolution Grand Challenge. The VC offers the promise of automatically proving that a program or component is correct, where correctness is defined by program assertions. While several VC prototypes exist, all adopt a semantics for assertions that is unsound. This paper presents a consolidation of VC requirements analysis activities that, in particular, brought us to ask targeted VC customers what kind of semantics they wanted. Taking into account both practitioners’ needs and current technological factors, we offer recovery of soundness through an adjusted definition of assertion validity that matches user expectations and can be implemented practically using current prover technology. For decades there have been debates concerning the most appropriate semantics for program assertions. Our contribution here is unique in that we have applied fundamental software engineering techniques by asking primary stakeholders what they want and based on this, proposed a means of efficiently realizing the semantics stakeholders want using standard tools and techniques. We describe how support for the new semantics has been added to ESC/Java2, one of the most fully developed VC prototypes. Case studies demonstrate the effectiveness of the new semantics at uncovering previously indiscernible specification errors.

PrePrint: Stressing Search with Scenarios for Flexible Solutions to Real-Time Task Allocation Problems

One of the most important properties of a good software engineering process and of the design of the software it produces is robustness to changing requirements. Scenario-based analysis is a popular method for improving the flexibility of software architectures. This paper demonstrates a search-based technique for automating scenario-based analysis in the software architecture deployment view. Specifically, a novel parallel simulated annealing search algorithm is applied to the real-time task allocation problem to find baseline solutions which require a minimal number of changes in order to meet the requirements of potential upgrade scenarios. Another simulated annealing based search is used for finding a solution which is similar to an existing baseline when new requirements arise. Solutions generated using a variety of scenarios are judged by how well they respond to different system requirements changes. The evaluation is performed on a set of problems with a controlled set of different characteristics.

PrePrint: Bayesian Approaches to Matching Architectural Diagrams

IT system architectures and many other kinds of structured artifacts are often described by formal models or informal diagrams. In practice, there are often a number of versions of a model or diagram, such as a series of revisions, divergent variants, or multiple views of a system. Understanding how versions correspond or differ is crucial, and thus automated assistance for matching models and diagrams is essential. We have designed a framework for finding these correspondences automatically based on Bayesian methods. We represent models and diagrams as graphs whose nodes have attributes such as name, type, connections to other nodes, and containment relations, and we have developed probabilistic models for rating the quality of candidate correspondences based on various features of the nodes in the graphs. Given the probabilistic models, we can find high quality correspondences using search algorithms. Preliminary experiments focusing on architectural models suggest that the technique is promising.

PrePrint: Service-Level Agreements for Electronic Services

The potential of communication networks and middleware to enable the composition of services across organisational boundaries remains incompletely realised. In this paper we argue that this is in part due to outsourcing risks, and describe the possible contribution of Service-Level Agreements (SLAs) to mitigating these risks. For SLAs to be effective, it should be difficult to disregard their original provisions in the event of a dispute between the parties. Properties of understandability, precision and monitorability ensure that the original intent of an SLA can be recovered, and compared to trustworthy accounts of service behaviour to resolve disputes fairly and without ambiguity. We describe the design and evaluation of a domain-specific language for SLAs that tend to exhibit these properties, and discuss the impact of monitorability requirements on service provision practices.

PrePrint: Reverse Engineering Input Syntactic Structure from Program Execution and Its Applications

Program input syntactic structure is essential for a wide range of applications such as test case generation, software debugging and network security. However, such important information is often not available (e.g., most malware programs make use of secret protocols to communicate) or not directly usable by machines (e.g., many programs specify their inputs in plain text or other random formats). Furthermore, many programs claim they accept inputs with a published format, but their implementations actually support a subset or a variant. Based on the observations that input structure is manifested by the way input symbols are used during execution and most programs take input with top-down or bottom-up grammars, we devise two dynamic analyses, one for each grammar category. Our evaluation on a set of real-world programs shows that our technique is able to precisely reverse engineer input syntactic structure from execution. We apply our technique to hierarchical delta debugging (HDD) and network protocol reverse engineering. Our technique enables the complete automation of HDD, in which programmers were originally required to provide input grammars, and improves the runtime performance of HDD. Our client study on network protocol reverse engineering also shows that our technique supersedes existing techniques.

PrePrint: An Experience in Testing the Security of Real-World Electronic Voting Systems

Voting is the process through which a democratic society determines its government. Therefore, voting systems are as important as other well-known critical systems, such as air traffic control systems or nuclear plant monitors. Unfortunately, voting systems have a history of failures that seems to indicate that their quality is not up to the task. Because of the alarming frequency and impact of these malfunctions, in recent years a number of vulnerability analysis exercises have been carried out against voting systems to determine if their confidentiality, integrity, and availability can be compromised. We have participated in two such large-scale projects, sponsored by the Secretaries of State of California and Ohio, in which the electronic voting machines used in those two states were tested. In our testing, we identified major flaws and implemented a number of attacks, which allowed us to take complete control of the examined voting systems. As a result of these evaluations, the Secretaries of State recommended changes to improve the security of the voting process. In this paper, we describe the methodology that we used in testing the two real-world electronic voting systems we evaluated, the findings of our analysis, our system-wide attacks, and the lessons we learned.

PrePrint: A Systematic Review of the Application and Empirical Investigation of Search-Based Test-Case Generation

Metaheuristic search techniques have been extensively used to automate the process of generating test cases and thus providing solutions for a more cost-effective testing process. This approach to test automation, often coined as “Search-based Software Testing” (SBST), has been used for a wide variety of test case generation purposes. Since SBST techniques are heuristic by nature, they must be empirically investigated in terms of how costly and effective they are at reaching their test objectives and whether they scale up to realistic development artifacts. However, approaches to empirically study SBST techniques have shown wide variation in the literature. This paper presents the results of a systematic, comprehensive review that aims at characterizing how empirical studies have been designed to investigate SBST cost-effectiveness and what empirical evidence is available in the literature regarding SBST cost-effectiveness and scalability. We also provide a framework that drives the data collection process of this systematic review and can be the starting point of guidelines on how SBST techniques can be empirically assessed. The intent is to aid future researchers doing empirical studies in SBST by providing an unbiased view of the body of empirical evidence and by guiding them in performing well designed empirical studies.