Modeling firmware as service functions and its application to test generation

Sunha Ahn, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationHardware and Software
Subtitle of host publicationVerification and Testing - 9th International Haifa Verification Conference, HVC 2013, Proceedings
PublisherSpringer Verlag
Number of pages17
ISBN (Print)9783319030760
StatePublished - 2013
Event9th Haifa Verification Conference, HVC 2013 - Haifa, Israel
Duration: Nov 5 2013Nov 7 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8244 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other9th Haifa Verification Conference, HVC 2013

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Modeling firmware as service functions and its application to test generation'. Together they form a unique fingerprint.

Cite this