A variety of meta-heuristic search algorithms have been introduced for optimising software release planning. However, there has been no comprehensive empirical study of different search algorithms across multiple different real world datasets. In this paper we present an empirical study of global, local and hybrid meta- and hyper-heuristic search based algorithms on 10 real world datasets. We find that the hyper-heuristics are particularly effective. For example, the hyper-heuristic genetic algorithm significantly outperformed the other six approaches (and with high effect size) for solution quality 85% of the time, and was also faster than all others 70% of the time. Furthermore, correlation analysis reveals that it scales well as the number of requirements increases.
Behavioral models are useful tools in understanding how programs work. Although, several inference approaches have been introduced to generate Extended Finite State Automatons from software execution traces, they suffer from accuracy, flexibility and decidability issues. In this study, we apply a hybrid technique to use both Reinforcement Learning and stochastic modeling to generate an Extended Probabilistic Finite State Automaton from software traces. Our approach is able to address the problems of inflexibility and un-decidability, reported in other state of the art approaches. Experimental results indicate that ReHMM outperforms other inference algorithms.
While developers are aware of the importance of comprehensively testing patches, the large effort involved in coming up with relevant test cases means that such testing rarely happens in practice. Furthermore, even when test cases are written to cover the patch, they often exercise the same behaviour in the old and the new version of the code. In this article, we present a symbolic execution-based technique that is designed to generate test inputs that cover the new program behaviours introduced by a patch. The technique works by executing both the old and the new version in the same symbolic execution instance, with the old version shadowing the new one. During this combined shadow execution, whenever a branch point is reached where the old and the new version diverge, we generate a test case exercising the divergence and comprehensively test the new behaviours of the new version. We evaluate our technique on the Coreutils patches from the CoREBench suite of regression bugs, and show that it is able to generate test inputs that exercise newly added behaviours and expose some of the regression bugs.
Self-adaptive software (SAS) can adapt itself under changing environment at runtime in order to optimize conflicting non-functional objectives, e.g., throughput and cost. We present FEMOSAA, a novel framework that automatically synergizes the feature model and Multi-Objective Evolutionary Algorithm (MOEA), to optimize SAS at runtime. FEMOSAA operates on two phases: at design time, FEMOSAA automatically transposes the design of SAS, expressed as a feature model, to the MOEA, creating new chromosome representation and reproduction operators. At runtime, FEMOSAA utilizes the feature model as domain knowledge to guide the MOEA, providing a larger chance for finding better solutions. Additionally, we designed a new method to find knee solutions, which yield a balanced trade-off. We conducted comprehensive experiments to evaluate FEMOSAA on two running SAS: one consists of RUBiS and various adaptable real-world software under the FIFA98 workload; another is a service-oriented SAS that can be dynamically composed by services. Particularly, we compared FEMOSAA against four of its variants and three other frameworks for SAS under various scenarios, including three commonly applied MOEAs, two workload patterns and diverse conflicting quality objectives. The results reveal the effectiveness of FEMOSAA and its superiority over the others with high statistical significance and non-trivial effect sizes.
The noble goal of software verification is to provide formal guarantees about the correctness of a program. In practice, however, automated verification remains elusive while automated testing experiences considerable traction. Yet, it seems testing provides no guarantees at all. Suppose, we are running the testing tool for seven days without finding an error. We cannot state with any degree of confidence that no bug exists. We cannot even make an informed decision whether it makes sense to continue or to abort the ongoing testing campaign. In this article, we develop a model of Software Testing and Analysis as Discovery of Species (STADS). We elicit an unexpected connection with the field of ecology and demonstrate how the STADS model can i) quantify the confidence that an ongoing testing campaign inspires in the program's correctness, ii) quantify the progress of an ongoing testing campaign towards completion, iii) extrapolate the current progress and confidence towards a given time in the future (e.g., to explore what-if scenarios), and iv) determine the expected time required if there is a certain progress to be achieved. Our empirical investigation demonstrates a good estimator performance (that improves with every generated test) for the state-of-the-art vulnerability detection tool, AFL.
CafeOBJ is a language for specifying a wide variety of software and hardware systems, and verifying properties of them. CafeOBJ makes it possible to verify properties by using either proof scores, which consists of reducing goal-related terms in user-defined modules, and by using theorem proving. While the former is more flexible, it lacks the formal support to ensure a property has been really proven. On the other hand, theorem proving might be too strict, and hence it hardens the verification of properties. In order to take advantage of the benefits of both techniques, we have extended CafeInMaude, a CafeOBJ interpreter implemented in Maude, with the CafeInMaude Proof Assistant (CiMPA) and the CafeInMaude Proof Generator (CiMPG). CiMPA is a proof assistant for proving inductive properties on CafeOBJ specifications that uses Maude metalevel features to allow programmers to create and manipulate CiMPA proofs. CiMPG provides a set of annotations for identifying proof scores and generating CiMPA scripts for these proof scores. We present CiMPA and CiMPG, detailing the behavior of CiMPA and the algorithm underlying CiMPG and illustrating the approach by using the QLOCK protocol. Finally, we present some benchmarks that give us confidence in the matureness and usefulness of these tools.
Architecture-centric development addresses the increasing complexity and variability of software systems by focusing on an architectural model, which is generally easier to understand and manipulate than source code. It requires a mechanism that can maintain architecture-implementation conformance during the architectural development and evolution. The challenge is twofold. There is an abstraction gap between software architecture and implementation, and the architecture may be frequently changed. Existing approaches are deficient in support for both change mapping and product line architecture. This paper presents a novel approach named 1.x-way mapping and its extension, 1.x-line mapping to support architecture-implementation mapping in single system development and in product line development respectively. They specifically address mapping architecture changes to code, maintaining variability conformance between product line architecture and code, and tracing architectural implementation. We built software tools named xMapper and xLineMapper to realize the two approaches, and conducted case studies with two existing open-source systems to evaluate the approaches.