Formal techniques for guaranteeing software correctness have made tremendous progress in recent decades. However, applying these techniques to real-world safety-critical systems remains challenging in practice. Inspired by goals set out in prior work, we report on a large-scale case study that applies modern verification techniques to check safety properties of a radiotherapy system in current clinical use. Because of the diversity and complexity of the system's components (software, hardware, and physical), no single tool was suitable for both checking critical component properties and ensuring that their composition implies critical system properties. This paper describes how we used state-of-the-art approaches to develop specialized tools for verifying safety properties of individual components, as well as an extensible tool for composing those properties to check the safety of the system as a whole. We describe the key design decisions that diverged from previous approaches and that enabled us to practically apply our approach to provide machine-checked guarantees. Our case study uncovered subtle safety-critical flaws in a pre-release of the latest version of the radiotherapy system's control software.

Particle radiotherapy facilities are highly capital intensive and must operate over decades to recoup the original investment. We describe the successful, long-term operation of a neutron radiotherapy center at the University of Washington, which has been operating continuously since September 1984. To date, 2836 patients have received neutron radiotherapy. The mission of the facility has also evolved to include the production of unique radioisotopes that cannot be made with the low-energy cyclotrons more commonly found in nuclear medicine departments. The facility is also used for neutron damage testing for industrial devices. In this paper, we describe the challenges of operating such a facility over an extended time period, including a planned maintenance and upgrade program serving diverse user groups, and summarize the major clinical results in terms of tumor control and normal tissue toxicity. Over time, the mix of patients being treated has shifted from common tumors such as prostate cancer, lung cancer, and squamous cell tumors of the head and neck to the rarer tumors such as salivary gland tumors and sarcomas due to the results of clinical trials. Current indications for neutron radiotherapy are described and neutron tolerance doses for a range of normal tissues presented.

The practical focus of this work is the dynamical simulation of polarization transport processes in quantum spin microscopy and spectroscopy. The simulation framework is built-up progressively, beginning with state-spaces (configuration manifolds) that are geometrically natural, introducing coordinates that are algebraically natural; and finally specifying dynamical potentials that are physically natural; in each respect explicit criteria are given for naturality. The resulting framework encompasses Hamiltonian flow (both classical and quantum), quantum Lindbladian processes, and classical thermostatic processes. Constructive validation and verification criteria are given for metric and symplectic flows on classical, quantum, and hybrid state-spaces, with particular emphasis to tensor network state-spaces. Both classical and quantum examples are presented, including dynamic nuclear polarization (DNP). A broad span of applications and challenges is discussed, ranging from the design and simulation of quantum spin microscopes to the design and simulation of quantum oracles.

Model programs are high-level behavioral specifications used for software testing and design analysis. Composition of model programs is a versatile technique that, at one end of the spectrum, enables one to build up larger models from smaller ones, and at the other end of the spectrum allows one to restrict larger models to specific scenarios. In this paper we provide a formal foundation for composition of model programs and investigate its use in various situations that arise in model program analysis.

Despite widespread OS, network, and hardware heterogeneity, there has been a lack of research into quantifying and improving portability of a programming environment. We have constructed a distributed testbed called Seattle built on a platform-independent programming API that is implemented on different operating systems and architectures. Our goal is to show that applications written to our API will be portable. In this work, we use an instrumented version of the programming environment for testing purposes. The instrumentation allows us to gather traces of actual program behavior from a running implementation. These traces can be used across different versions of the implementation exactly as if they were test cases generated offline from a model program, so we can commence testing using model based testing tools, without constructing a model program. Such offline testing is only effective in scenarios where traces are expected to be reproducible (deterministic). Where reproducibility is not expected, for instance due to nondeterminism in the network environment, we must resort to on-the-fly testing, which does require a model program. To validate this model program, we can use the recorded traces of actual behavior. Validating with captured traces should provide greater coverage than we could achieve by validating only with traces constructed a priori.

We show how model-based on-the-fly testing can be applied in the context of web applications using the NModel toolkit. The concrete case study is a commercial web-based positioning system called WorkForce Management (WFM) which interacts with a number of other services, such as billing and positioning, through a mobile operator. We describe the application and the testing, and discuss the test results.

This book teaches model-based analysis and model-based testing, with important new ways to write and analyze software specifications and designs, generate test cases, and check the results of test runs. These methods increase the automation in each of these steps, making them more timely, more thorough, and more effective. Using a familiar programming language, testers and analysts will learn to write models that describe how a program is supposed to behave. The authors work through several realistic case studies in depth and detail, using a toolkit built on the C# language and the .NET framework. Readers can also apply the methods in analyzing and testing systems in many other languages and frameworks. Intended for professional software developers including testers, and for university students, this book is suitable for courses on software engineering, testing, specification, or applications of formal methods.