Synthesizing Operating System Based Device Drivers in Embedded Systems

Shaojie Wang, Sharad Malik

Research output: Contribution to conferencePaperpeer-review

21 Scopus citations

Abstract

This paper presents a correct-by-construction synthesis method for generating operating system based device drivers from a formally specified device behavior model. Existing driver development is largely manual using an ad-hoc design methodology. Consequently, this task is error prone and becomes a bottleneck in embedded system design methodology. Our solution to this problem starts by accurately specifying device access behavior with a formal model, viz. extended event driven finite state machines. We state easy to check soundness conditions on the model that subsequently guarantee properties such as bounded execution time and deadlock-free behavior. We design a deadlock-free resource accessing scheme for our device access model. Finally, we synthesize an operating system (OS) based event processing mechanism, which is the core of the device driver, using a disciplined methodology that assures the correctness of the resulting driver. We validate our synthesis method using two case studies: an infrared port and the USB device controller for an SA 1100 based handheld. Besides assuring a correct-by -construction driver, the size of the specification is 70% smaller than a manually written driver, which is a strong indicator of improved design productivity.

Original languageEnglish (US)
Pages37-44
Number of pages8
DOIs
StatePublished - Dec 1 2003
EventFirst IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2003 - Newport Beach, CA, United States
Duration: Oct 1 2003Oct 3 2003

Other

OtherFirst IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2003
CountryUnited States
CityNewport Beach, CA
Period10/1/0310/3/03

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Synthesizing Operating System Based Device Drivers in Embedded Systems'. Together they form a unique fingerprint.

Cite this