Abstract Context Program synthesis is the task of automatically finding a program that satisfies the user intention. In previous work, we developed APS‐GA, a program synthesizer based on a genetic algorithm. As genetic algorithms depend on a fitness function, so does APS‐GA. Researchers argue that different distance metrics for a fitness function may reveal behavioral differences in the genetic algorithm. More recently, we presented initial evidence that APS‐GA was not affected by different distance metrics for its fitness function. However, that study was carried out on a medium‐sized scale. Objective In order to investigate our previous study on a larger scale, we extended our experiment to replicate it on a search space that is up to 6500 times larger than our previous work, and we ran it with a synthesis time that was at least 20 times longer. We have chosen the same five distance metrics as fitness functions to check whether they affect the synthesis task of five integer domain imperative toy programs. Method A hypothesis test was proposed and experiments were conducted to observe the number of calls to the fitness function () and to measure the synthesis time (). Results By considering a confidence level of 95% (with ), we found out that there were no significant differences in both and . Conclusion With these results, our extended replication study suggests that the discrete distance metric constitutes the best choice for APS‐GA as it guides the search with the same effectiveness as the other metrics, and is cheaper to compute.

Soccer is a hugely popular sport globally and boasts a billion-dollar industry. ML (Machine Learning) algorithms have been adopted to predict outcomes in soccer. However, soccer matches are sometimes difficult to predict even by well informed experts and in other cases have surprising results. In the same sense, ML predictions may be unreliable and inaccurate. In this paper, we investigate a new approach in the ML literature, called assessors, adopted in our work to monitor the quality of predictions of a ML base model along a championship in order to identify the most reliable ones. Given a match, the assessor is used to predict whether the base model is able to correctly predict that match's result. Unreliable predictions are then rejected by the assessor. Our goal is to optimize the accuracy of accepted predictions while controlling the rejection rate. We conducted experiments on real data to identify the championships, teams, and rounds where the proposed rejection option approach performs best. The innovative proposed approach was actually useful to identify high-quality predictions, thus enhancing the reliability of match outcome predictions.

Abstract Context Program synthesis is the task of automatically finding a program that satisfies the user intention. In previous work, we have developed a program synthesizer that integrates genetic algorithm with model finder. A genetic algorithm uses a fitness function to calculate how “distant to a solution” a given candidate program is. Researchers argue that different distance metrics for a fitness function may reveal behavioral differences in the genetic algorithm. Objective We have chosen five distance metrics as fitness functions to check whether they affect the synthesis task of five different integer domain imperative toy‐programs which read/write integer values using fundamental syntactic constructs, such as while, if‐then‐else, and so forth. We have used input/output examples and sketches to constrain the search space of the candidate programs. Method A hypothesis test was proposed and experiments were conducted to observe the number of calls to the fitness function (x) and to measure the synthesis time ( ). Results Regarding x, the synthesizer found a solution for all five subjects after calling the fitness function the same amount of times. For , a one‐way ANOVA was performed with a significance level of 5% ( ). No significant differences were observed in both x and . Conclusion With these preliminary results, this study suggests that the discrete distance metric is the best choice, because it guides the search with the same effectiveness as the others and is not time consuming, and so forth. However, future experimentation with a larger search space will confirm or not this initial impression.

In this paper we propose a way to find weights of a ranking function semi-automatically.From the manual choices made by (experienced) human test architects, our idea is to propose an optimization model that tries to find the necessary weights automatically.We present some experiments by encoding our optimization model in the Z3 SMT solver and using real Motorola Mobility 1 data.

Abstract In previous work we presented a CSP-based systematic approach that fosters the rigorous design of component-based development. Our approach is strictly defined in terms of composition rules, which are the only permitted way to compose components. These rules guarantee the preservation of properties (particularly deadlock freedom) by construction in component composition. Nevertheless, their application is allowed only under certain conditions whose verification via model checking turned out impracticable even for some simple designs, and particularly those involving cyclic topologies. In this paper, we address the performance of the analysis and present a significantly more efficient alternative to the verification of the rule side conditions, which are improved by carrying out partial verification on component metadata throughout component compositions and by using behavioural patterns. The use of metadata, together with behavioural patterns, demands new composition rules, which allow previous exponential time verifications to be carried out now in linear time. Two case studies (the classical dining philosophers, also used as a running example, and an industrial version of a leadership election algorithm) are presented to illustrate and validate the overall approach.

Abstract A model checker is an automatic tool that traverses a specific structure (normally a Kripke structure referred as the modelM) to check the satisfaction of some (temporal) logical propertyf. This is formally stated as M⊧f . For some formal notations, the modelMof a specificationS(written in a formal languageL) can be described as a labelled transition system (LTS). Specifically, it is not clear in general how usual tools such as SPIN, FDR, PAT, etc., create the LTS representation from a given process. Although one expects the coherence of the LTS generation with the semantics ofL, it is completely hidden inside the model checker itself. In this paper we show how to create a model checker forL, using a development approach based on its operational semantics. We use a systematic semantics embedding and the formal modeling using logic programming and analysis (FORMULA) framework to this end. We illustrate our strategy considering the formal language COMPASS modelling language (CML)—a new language that was based on CSP, VDM and the refinement calculus proposed for modelling and analysis of systems of systems. As FORMULA is based on satisfiability modulo theories solving, our model checker can handle communications and predicates involving data with infinite domains by building and manipulating a symbolic LTS. This goes beyond the capabilities of traditional CSP model checkers such as FDR and PAT. Moreover, we show how to reduce time and space complexities by simple semantic modifications in the embedding. This allows a more semantics-preserving tuning. Finally, we show a real implementation of our model checker in an integrated development platform for CML and its practical use on an industrial case study.

Abstract We present a strategy for the automatic generation of test cases from parametrised use case templates that capture control flow, state, input and output. Our approach allows test scenario selection based on particular traces or states of the model. The templates are internally represented as CSP processes with explicit input and output alphabets, and test generation is expressed as counter-examples of refinement checking, mechanised using the FDR tool. Soundness is addressed through an input–output conformance relation formally defined in the CSP traces model. This purely process algebraic characterisation of testing has some potential advantages, mainly an easy automation of conformance verification and test case generation via model checking, without the need to develop any explicit algorithm.

SUMMARY This paper mechanises conformance verification in the setting of the CSP process algebra. The verification strategy is captured by a theorem stated as a process refinement expression, which can be verified by a model checker such as FDR. The conformance relation,cspio, distinguishes input and output events. The process algebraic framework of CSP is used to address compositional conformance verification by establishing compositionality properties forcspiowith respect to the CSP operators. Althoughcspiohas been defined in the standard CSP traces model, one can address quiescence situations using a special output event, in which case it is formally established thatcspiois equivalent to Tretmansioco. All the results have been mechanically proved using the CSP‐Prover. The proposed testing theory has been adopted in an industrial context involving collaboration with Motorola, on testing mobile applications. Several examples and a case study are presented to illustrate the overall approach. Copyright © 2013 John Wiley & Sons, Ltd.

Although it is assumed that the implementation of design by contract is better modularized by means of aspect-oriented (AO) programming, there is no empirical evidence on the effectiveness of AO for modularizing non-trivial design by contract code in realistic development scenarios. This paper reports a quantitative and qualitative case study that evolves a real-life application to assess various facets of the adequacy of aspects for modularizing the design by contract concern. Our evaluation focused upon a number of system changes that are typically performed during software maintenance tasks. The study was driven by an analysis of fundamental modularity attributes, such as separation of concerns, coupling, conciseness, and change propagation. We have found that AO techniques improved separation of concerns and the design stability between the design by contract code and base application code throughout the development scenarios. However, contradicting the general intuition, the AO versions of the system did not present significant gains regarding four classical size metrics we employed.

There are works that propose metamodels for SDW modeling. However, we observe that most of these works defines metamodels that mix concepts of DW modeling with concepts of the OLAP cube modeling. We disagree with this view, because we understand that a DW is essentially a database, which can be analyzed/queried by any data analysis tool. Moreover, we also note other limitations. For example: the most proposed metamodels 1) do not support important techniques for DW modeling and 2) represent the spatiality in a SDW stereotyping the dimensions and fact tables as spatial or hybrid, rather than simply stereotyping the attributes/measures as spatial. Aiming to solve these problems we propose a more straightforward and more expressive metamodel for SDW modeling, named Spatial Data Warehouse Metamodel (SDWM), which describes the constructors and the restrictions needed to model and validate a SDW schema. As a proof of concept, we implemented a CASE tool according to our metamodel and, with this CASE tool, we designed a SDW for the Meteorological Laboratory from the State of Pernambuco, in Brazil.

Design by Contract (DbC) is a technique for developing and improving functional software correctness through definition of "contracts" between client classes and their suppliers. Such contracts are enforced during runtime and if any of them is violated a runtime error should occur. Runtime assertions checkers (RACs) are a well-known technique that enforces such contracts. Although they are largely used to implement the DbC technique in contemporary languages, like Java, studies have shown that characteristics of contemporary exception handling mechanisms can discard contract violations detected by RACs. As a result, a contract violation may not be reflected in a runtime error, breaking the supporting hypothesis of DbC. This paper presents an error recovery technique for RACs that tackles such limitations. This technique relies on aspect-oriented programming in order to extend the functionalities of existing RACs stopping contract violations from being discarded. We applied the recovery technique on top of five Java-based contemporary RACs (i.e., JML/jml, JML/ajml, JContractor, CEAP, and Jose). Preliminary results have shown that the proposed technique could actually prevent the contract violations from being discarded regardless of the characteristics of the exception handling code of the target application.

Industry uses different testing techniques for test case generation and execution. But in general no systematic evaluation is performed to identify which technique is better (for instance, to find bugs faster). This paper presents a statistical assessment of two GUI testing techniques, BxT and DH, which are used on Motorola phone applications. These techniques test applications by pressing certain phone keys, from certain screens and during some amount of time. We consider three exploration parameters for each technique in our design and analysis of experiments: Driven determines whether a test case always starts from a single initial state (screen) or set of initial states; KeyProb associates an occurrence probability for SizeTC refers to the number of steps a test can have (a fourth parameter is the Technique itself). As conclusions, we show that BxT is better than DH and the SizeTC and the Technique parameters and the combination Driven*SizeTC have significant effects on the time to find a bug.

Models abstract reality. Although abstract, such models can capture the essence of real world phenomena as long as they are sufficiently accurate. The development of new techniques or its usage in a different environment cannot always be satisfactory and can be expensive. In this paper we propose a novel strategy to create GUI probabilistic testing models and calibrating them with the aid of real experiments based on survival analysis. Survival analysis is used to transform exact responses of the real experiment into probabilistic predictions, comparable to the responses obtained from our testing models. Thus calibration means searching for model parameter instances that yield model predictions almost equal to survival analysis predictions. Using our strategy, we improved the accuracy of our models showing that the models has a result closely with a real experiment.

This paper reports an empirical evaluation of four black-box testing techniques for crashing programs through their GUI interface: SH, AF, DH, and BxT. The techniques vary in their level of automation and the results they offer. The experiments we conducted quantify execution time and the capability of finding a crash for each technique on 8 different cellular phone configurations with historical (real) errors. The results show that AF and BxT offered better precision (i.e., the fraction of runs that end in a crash out of the total number of runs) than SH and DH (AF and BxT found crashes in all 8 configurations), and BxT crashes the application the fastest more often (5 out of 8 cases). The experiments reveal that the selection of the random seed to AF and BxT results in a high variance of execution time (i.e., the time the technique takes to either crash the application or timeout in 40h): the mean (across 8 phone configurations) of the standard deviation of execution times (for 10 runs per each phone configuration) is 7.79h for AF and 5.21h for BxT. Despite this fact, AF and BxT could crash the application consistently: the mean of the precision (fraction of the 10 runs that results in a crash) is 74% for AF and 69% for BxT.

Different testing techniques are being proposed in software testing to improve systems quality and increase development productivity. However, it is difficult to determine from a given set of testing techniques, which is the most effective testing technique for a certain domain, particularly if they are random-based. We are proposing a strategy and a framework that can evaluate such testing techniques. Our framework is defined compositionally and parametric ally. This allows us to characterize different aspects of systems in an incremental way as well as test specific hypothesis about the system under test. In this paper we focus on GUI-based systems. That is, the specific internal behavior of the system is unknown but it can be approximated by probabilistic behaviors. And the empirical evaluation is based on the probabilistic model checker PRISM.