Static Checking of Interrupt-Driven Software

Sep 06, 2000

PDF
Download: MP4 Video Size: 200.9MB  
Watch on YouTube

Abstract

Resource-constrained devices are becoming ubiquitous. Examples include cell phones, palm pilots, and digital thermostats. It can be difficult to fit required functionality into such a device without sacrificing the simplicity and clarity of the software.

Increasingly complex embedded systems require extensive brute-force testing, making development and maintenance costly. This is particularly true for system components that are written in assembly language. Static checking has the potential of alleviating these problems, but until now there has been little tool support for programming at the assembly level.

In this paper we present the design and implementation of a static checker for interrupt-driven Z86-based software with hard real-time requirements. For six commercial microcontrollers, our checker has produced upper bounds on interrupt latencies and stack sizes, as well as verified fundamental safety and liveness properties. Our approach is based on a known algorithm for model checking of pushdown systems, and produces a control-flow graph annotated with information about time, space, safety, and liveness. Each benchmark is approximately 1000 lines of code, and the checking is done in a few seconds on a standard PC.

Our tool is one of the first to give an efficient and useful static analysis of assembly code. It enables increased confidence in correctness, significantly reduced testing requirements, and support for maintenance throughout the system life-cycle. Joint work with Dennis Brylow and Niels Damgaard.