[M.Sc. Teamproject] Case Study: Verified USB Driver

Today, configuration and control of small embedded systems via PCs makes use of the classical serial RS232 interface.  On the one hand, modern PCs don't provide such an interface any more.  On the other hand, even small contemporary controllers employed in embedded systems often comprise an on-board USB port.  Therefore, users rightly expect tomorrow's embedded systems to interact seamlessly with the PC via USB ports.

The problem with embedded devices considered in this project is, that there are typically no standard drivers for the controller side.    The reason is simply, that these devices often don't even run an operating system which could provide a framework for a driver.  The controller manufacturer only provides exemplary implementations.  On the PC side, the problem is that the driver is supposed to be of high quality because the controlled embedded system may be critical.

In this project, the candidate is supposed to develop USB drivers for both sides.  The research task is to assess, on the one hand, the quality that can be ensured with static driver verification tools provided by Co.  Microsoft and on the other hand to assess in how far state-of-the-art software engineering methods can ensure quality of the USB driver on the controller side.

The candidate should have a fair background in software-engineering, interest in software development for embedded systems (in C), and at best some background in formal methods.

Note: This is a joint project with company SeCa GmbH. The project is supposed to be conducted as part of a 9 month internship (``Werkstudent'') where the candidate is employed as a student worker at SeCa.

• usb_driver_seca-20091208-1.pdf