Static Checking of Interrupt-Driven Software
Jens Palsberg - CERIAS
Sep 06, 2000PDF () Size: 200.9MB
Download: MP4 Video
Watch in your Browser Watch on YouTube
AbstractResource-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 SpeakerJens 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.
The views, opinions and assumptions expressed in these videos are those of the presenter and do not necessarily reflect the official policy or position of CERIAS or Purdue University. All content included in these videos, are the property of Purdue University, the presenter and/or the presenter’s organization, and protected by U.S. and international copyright laws. The collection, arrangement and assembly of all content in these videos and on the hosting website exclusive property of Purdue University. You may not copy, reproduce, distribute, publish, display, perform, modify, create derivative works, transmit, or in any other way exploit any part of copyrighted material without permission from CERIAS, Purdue University.