Document Type

Conference Proceeding

Language

eng

Format of Original

10 p.

Publication Date

5-12-2001

Publisher

Institute of Electrical and Electronics Engineers (IEEE)

Source Publication

Proceedings of the 23rd International Conference on Software Engineering, 2001 (ICSE 2001)

Source ISSN

0270-5257

Abstract

Resource-constrained devices are becoming ubiquitous. Examples include cell phones, Palm Pilots and digital thermostats. It can be difficult to fit the 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 the 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 code correctness, significantly reduced testing requirements and support for maintenance throughout the system life-cycle.

Comments

Accepted version. Published as part of the Proceedings of the 23rd International Conference on Software Engineering, 2001 (ICSE 2001): 47-56. DOI. © 2001 The Institute of Electrical and Electronics Engineers. Used with permission.

Dennis Brylow was affiliated with Purdue University at the time of publication.

Download
brylow_8563acc.docx (151 kB)
ADA Accessible Version

Share

COinS