Modeling firmware as service functions and its application to test generation

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.