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.

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.