Jens Palsberg, Static Checking of Interrupt-Driven Software

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. About the speaker: Jens Palsberg received a Ph.D. in Computer Science from University of Aarhus, Denmark in 1992. In 1992-1996 he was a visiting scientist at various institutions, including MIT. In 1996 he joined the faculty at Purdue University where he is an Associate Professor of Computer Science. His research interests are programming languages, compilers, software engineering, and software security. He has authored over 50 technical papers in these areas. His 1994 book with Michael Schwartzbach is entitled Object-oriented Type Systems. In 1998 he received the National Science Foundation Faculty Early Career Development Award, and in 1999 he received the Purdue University Faculty Scholar award. Dr. Palsberg\'s research has been supported by NSF, DARPA, IBM, and British Telecom. He is a member of the editorial board of IEEE Transactions on Software Engineering.