Explore the vast range of titles available.

This book gives a practical introduction to model-based testing, showing how to write models for testing purposes and how to use model-based testing tools to generate test suites. It is aimed at testers and software developers who wish to use model-based testing, rather than at tool-developers or academics.The book focuses on the mainstream practice of functional black-box testing and covers different styles of models, especially transition-based models (UML state machines) and pre/post models (UML/OCL specifications and B notation). The steps of applying model-based testing are demonstrated on examples and case studies from a variety of software domains, including embedded software and information systems. From this book you will learn:* The basic principles and terminology of model-based testing* How model-based testing differs from other testing processes* How model-based testing fits into typical software lifecycles such as agile methods and the Unified Process* The benefits and limitations of model-based testing, its cost effectiveness and how it can reduce time-to-market* A step-by-step process for applying model-based testing* How to write good models for model-based testing* How to use a variety of test selection criteria to control the tests that are generated from your models* How model-based testing can connect to existing automated test execution platforms such as Mercury Test Director, Java JUnit, and proprietary test execution environments * Presents the basic principles and terminology of model-based testing* Shows how model-based testing fits into the software lifecycle, its cost-effectiveness, and how it can reduce time to market* Offers guidance on how to use different kinds of modeling techniques, useful test generation strategies, how to apply model-based testing techniques to real applications using case studies

The quest to develop increasingly sophisticated verification systems continues unabated. Tools such as Dafny, Spec#, ESC/Java, SPARK Ada and Whiley attempt to seamlessly integrate specification and verification into a programming language, in a similar way to type checking. A common integration approach is to generate verification conditions that are handed off to an automated theorem prover. This provides a nice separation of concerns and allows different theorem provers to be used interchangeably. However, generating verification conditions is still a difficult undertaking and the use of more “high-level” intermediate verification languages has become commonplace. In particular, Boogie provides a widely used and understood intermediate verification language. A common difficulty is the potential for an impedance mismatch between the source language and the intermediate verification language. In this paper, we explore the use of Boogie as an intermediate verification language for verifying programs in Whiley. This is noteworthy because the Whiley language has (amongst other things) a rich type system with considerable potential for an impedance mismatch. We provide a comprehensive account of translating Whiley to Boogie which demonstrates that it is possible to model most aspects of the Whiley language. Key challenges posed by the Whiley language included: the encoding of Whiley’s expressive type system and support for flow typing and generics; the implicit assumption that expressions in specifications are well defined; the ability to invoke methods from within expressions; the ability to return multiple values from a function or method; the presence of unrestricted lambda functions; and the limited syntax for framing. We demonstrate that the resulting verification tool can verify significantly more programs than the native Whiley verifier which was custom-built for Whiley verification. Furthermore, our work provides evidence that Boogie is (for the most part) sufficiently general to act as an intermediate language for a wide range of source languages.

Usually, test automation scripts for a web application directly mirror the actions that the tester carries out in the browser, but they tend to be verbose and repetitive, making them expensive to maintain and ineffective in an agile setting. Our research has focussed on providing tool-support for business-level, example-based specifications that are mapped to the browser level for automatic verification. We provide refactoring support for the evolution of existing browser-level tests into business-level specifications. As resulting business rule tables may be incomplete, redundant or contradictory, our tool provides feedback on coverage.

Purpose This paper describes dynamic agent composition , used to support the development of flexible and extensible large-scale agent-based models (ABMs). This approach was motivated by a need to extend and modify, with ease, an ABM with an underlying networked structure as more information becomes available. Flexibility was also sought after so that simulations are set up with ease, without the need to program. Methods The dynamic agent composition approach consists in having agents, whose implementation has been broken into atomic units, come together at runtime to form the complex system representation on which simulations are run. These components capture information at a fine level of detail and provide a vast range of combinations and options for a modeller to create ABMs. Results A description of the dynamic agent composition is given in this paper, as well as details about its implementation within MODAM ( MOD ular A gent-based M odel), a software framework which is applied to the planning of the electricity distribution network. Illustrations of the implementation of the dynamic agent composition are consequently given for that domain throughout the paper. It is however expected that this approach will be beneficial to other problem domains, especially those with a networked structure, such as water or gas networks. Conclusions Dynamic agent composition has many advantages over the way agent-based models are traditionally built for the users, the developers, as well as for agent-based modelling as a scientific approach. Developers can extend the model without the need to access or modify previously written code; they can develop groups of entities independently and add them to those already defined to extend the model. Users can mix-and-match already implemented components to form large-scales ABMs, allowing them to quickly setup simulations and easily compare scenarios without the need to program. The dynamic agent composition provides a natural simulation space over which ABMs of networked structures are represented, facilitating their implementation; and verification and validation of models is facilitated by quickly setting up alternative simulations.

Usually, test automation scripts for a web application directly mirror the actions that the tester carries out in the browser, but they tend to be verbose and repetitive, making them expensive to maintain and ineffective in an agile setting. Our research has focussed on providing tool-support for business-level, example-based specifications that are mapped to the browser level for automatic verification. We provide refactoring support for the evolution of existing browser-level tests into business-level specifications. As resulting business rule tables may be incomplete, redundant or contradictory, our tool provides feedback on coverage.

Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms. However, in order to facilitate sharing of common subexpressions, modern compilers represent expressions as term graphs. Defining the semantics of term graphs is more complicated than defining the semantics of their equivalent term representations. More significantly, defining optimizations directly on term graphs and proving semantics preservation is considerably more complicated than on the equivalent term representations. On terms, optimizations can be expressed as conditional term rewriting rules, and proofs that the rewrites are semantics preserving are relatively straightforward. In this paper, we explore an approach to using term rewrites to verify term graph transformations of optimizations within the GraalVM compiler. This approach significantly reduces the overall verification effort and allows for simpler encoding of optimization rules.

We describe the verification of an existing smart contract for a simple casino application, using the Whiley specification and programming language, with a fully automated verification engine based on Boogie and Z3. After finding and fixing several specification and code issues in the smart contract, we are able to verify all the operations of the smart contract.

Automated Program Repair (APR) has emerged as a promising paradigm for reducing debugging time and improving the overall efficiency of software development. Recent advances in Large Language Models (LLMs) have demonstrated their potential for automated bug fixing and other software engineering tasks. Nevertheless, the general-purpose nature of LLM pre-training means these models often lack the capacity to perform project-specific repairs, which require understanding of domain-specific identifiers, code structures, and contextual relationships within a particular codebase. As a result, LLMs may struggle to generate correct patches when the repair depends on project-specific information. To address this limitation, we introduce RelRepair, a novel approach that retrieves relevant project-specific code to enhance automated program repair. RelRepair first identifies relevant function signatures by analyzing function names and code comments within the project. It then conducts deeper code analysis to retrieve code snippets relevant to the repair context. The retrieved relevant information is then incorporated into the LLM's input prompt, guiding the model to generate more accurate and informed patches. We evaluate RelRepair on two widely studied datasets, Defects4J V1.2 and ManySStuBs4J, and compare its performance against several state-of-the-art LLM-based APR approaches. RelRepair successfully repairs 101 bugs in Defects4J V1.2. Furthermore, RelRepair achieves a 17.1\\% improvement in the ManySStuBs4J dataset, increasing the overall fix rate to 48.3\\%. These results highlight the importance of providing relevant project-specific information to LLMs, shedding light on effective strategies for leveraging LLMs in APR tasks.

The optimization phase of a compiler is responsible for transforming an intermediate representation (IR) of a program into a more efficient form. Modern optimizers, such as that used in the GraalVM compiler, use an IR consisting of a sophisticated graph data structure that combines data flow and control flow into the one structure. As part of a wider project on the verification of optimization passes of GraalVM, this paper describes a semantics for its IR within Isabelle/HOL. The semantics consists of a big-step operational semantics for data nodes (which are represented in a graph-based static single assignment (SSA) form) and a small-step operational semantics for handling control flow including heap-based reads and writes, exceptions, and method calls. We have proved a suite of canonicalization optimizations and conditional elimination optimizations with respect to the semantics.

TypeScript is a quickly evolving superset of JavaScript with active development of new features. Our paper seeks to understand how quickly these features are adopted by the developer community. Existing work in JavaScript shows the adoption of dynamic language features can be a major hindrance to static analysis. As TypeScript evolves the addition of features makes the underlying standard more and more difficult to keep up with. In our work we present an analysis of 454 open source TypeScript repositories and study the adoption of 13 language features over the past three years. We show that while new versions of the TypeScript compiler are aggressively adopted by the community, the same cannot be said for language features. While some experience strong growth others are rarely adopted by projects. Our work serves as a starting point for future study of the adoption of features in TypeScript. We also release our analysis and data gathering software as open source in the hope it helps the programming languages community.