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.