Abstract This paper proposes a new methodology for early validation of high-level requirements on cyber-physical systems with the aim of improving their quality and, thus, lowering chances of specification errors propagating into later stages of development where it is much more expensive to fix them. The paper presents a transformation of a real-world requirements specification of a medical device—the Patient-Controlled Analgesia (PCA) Pump—into an Event Calculus model that is then evaluated using Answer Set Programming and the s(CASP) system. The evaluation under s(CASP) allowed deductive as well as abductive reasoning about the specified functionality of the PCA pump on the conceptual level with minimal implementation or design dependent influences and led to fully automatically detected nuanced violations of critical safety properties. Further, the paper discusses scalability and non-termination challenges that had to be faced in the evaluation and techniques proposed to (partially) solve them. Finally, ideas for improving s(CASP) to overcome its evaluation limitations that still persist as well as to increase its expressiveness are presented.

This paper describes Unite, a new tool intended as an adapter for transforming non-interactive command-line analysis tools to OSLC-compliant web services. Unite aims to make such tools easier to adopt and more convenient to use by allowing them to be accessible, both locally and remotely, in a unified way and to be easily integrated into various development environments. Open Services for Lifecycle Collaboration (OSLC) is an open standard for tool integration and was chosen for this task due to its robustness, extensibility, support of data from various domains, and its growing popularity. The work is motivated by allowing existing analysis tools to be more widely used with a strong emphasis on widening their industrial usage. We have implemented Unite and used it with multiple existing static as well as dynamic analysis and verification tools, and then successfully deployed it internationally in the industry to automate verification tasks for development teams in Honeywell. We discuss Honeywell's experience with using Unite and with OSLC in general. Moreover, we also provide the Unite Client (UniC) for Eclipse to allow users to easily run various analysis tools directly from the Eclipse IDE.

The paper presents advances in the ANaConDA framework for dynamic analysis and testing of concurrent C/C++ programs. ANaConDA comes with several built-in analysers, covering detection of data races, deadlocks, or contract violations, and allows for an easy creation of new analysers. To increase the variety of tested interleavings, ANaConDA offers various noise injection techniques. The framework performs the analysis on a binary level, thus not requiring the source code of the program to be available. Apart from many academic experiments, ANaConDA has also been successfully used to discover various errors in industrial code.

The central notion of this paper is that of contracts for concurrency, allowing one to capture the expected atomicity of sequences of method or service calls in a concurrent program. The contracts may be either extracted automatically from the source code, or provided by developers of libraries or software modules to reflect their expected usage in a concurrent setting. We start by extending the so-far considered notion of contracts for concurrency in several ways, improving their expressiveness and enhancing their applicability in practice. Then, we propose two complementary analyses—a static and a dynamic one—to verify programs against the extended contracts. We have implemented both approaches and present promising experimental results from their application on various programs, including real-world ones where our approach unveiled previously unknown errors.

Summary Testing of concurrent software written in programming languages like Java and C/C++ is a highly challenging task owing to the many possible interactions among threads. A simple, cheap, and effective approach that addresses this challenge is testing with noise injection , which influences the scheduling so that different interleavings of concurrent actions are witnessed. In this paper, multiple results achieved recently in the area of noise‐injection‐based testing by the authors are presented in a unified and extended way. In particular, various concurrency coverage metrics are presented first. Then, multiple heuristics for solving the noise placement problem (i.e. where and when to generate noise) as well as the noise seeding problem (i.e. how to generate the noise) are introduced and experimentally evaluated. In addition, several new heuristics are proposed and included into the evaluation too. Recommendations on how to set up noise‐based testing for particular scenarios are then given. Finally, a novel use of the genetic algorithm for finding suitable combinations of the many parameters of tests and noise techniques is presented. Copyright © 2014 John Wiley & Sons, Ltd.