Hardware and Software: Verification and Testing

The term firmware refers to software that is tied to a specific hardware platform, e.g., low-level drivers that physically interface with the peripherals. More recently, this has grown to include software that manages critical hardware platform functions such as power management. This growing firmware needs to be shipped with the hardware and shares many of the same critical design concerns as the hardware. The two that we address in this paper are: co-design with the other system components, and validation of the firmware interactions with the connected hardware modules. To this end we introduce a specific Service-Function Transaction-Level Model (TLM) for modeling the firmware and interacting hardware components. A service function provides a service in response to a specific trigger, much like an interrupt-service routine responding to an interrupt. While TLM has been used in the past for HW-SW codesign, we show how the particular structure of the proposed service function based model is useful in the context of firmware design. Specifically, we show its application in automatic test generation. Recently concolic testing has emerged as an automated technique for test generation for single-threaded software. This technique cannot be used directly for firmware, which, by definition, runs in parallel with the interacting hardware modules. We show how the service function model proposed here can be used to analyze these interactions and how single-threaded concolic testing can still be used for an important class of these interaction patterns. The model and the test generation are illustrated through a non-trivial case study of the open-source Rockbox MP3 player.

Testing web-based software infrastructures is challenging. The need to interact with different services running on different devices, with different expectations for security and privacy contributes not only to the complexity of the infrastructure, but also to the approaches necessary to test it. Moreover, as large-scale systems, such infrastructures may be developed by distributed teams simultaneously making changes to APIs and critical components that implement them. In this paper, we describe our experiences testing one such infrastructure – the webinos software platform – and the lessons learned tackling the challenges faced. While ultimately these challenges were impossible to overcome, this paper explores the techniques that worked most effectively and makes recommendations for developers and teams in similar situations. In particular, our experiences with continuous integration and automated testing processes are described and analysed.

We address this problem and propose to filter mutations according to the attention the designer has paid to the mutated components in the model. We formalize the attention intuition using a multi-valued setting, where the truth values of the signals in the model describe their level of importance. Non-covered mutations of signals of high importance are then more alarming than non-covered mutations of signals with low intention. Given that such “importance information” is usually not available in practice, we suggest two new coverage metrics that automatically approximate it. The idea behind both metrics is the observation that designers tend to modify the value of signals only when there is a reason to do so. We demonstrate the advantages of both metrics and describe algorithms for calculating them.

The success of software model checking depends on finding an appropriate abstraction of the program to verify. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types (e.g., ‘int’ and ‘long’) to guide the selection of an appropriate abstract domain for a model checker. Our implementation on top of an existing verification framework determines the domain type for each variable in a pre-analysis step, based on the usage of variables in the program, and then assigns each variable to an abstract domain. Based on a series of experiments on a comprehensive set of verification tasks from international verification competitions, we demonstrate that the choice of the abstract domain per variable (we consider one explicit and one symbolic domain) can substantially improve the verification in terms of performance and precision.

Consider the problem of partitioning a number of concurrent interacting processes into a smaller number of physical processors. The performance and efficiency of such a system critically depends on the tasks that the processes perform and the partitioning scheme. Although empirical measurements have been extensively used a posteriori to assess the success of partitioning, the results only focus on a subset of possible executions and cannot be generalized. In this paper, we propose a probabilistic state exploration method to evaluate a priori the efficiency of a set of partitions in terms of the speedup they achieve for a given model. Our experiments show that our method is quite effective in identifying partitions that result in better levels of parallelism.