Document Type

Article

Language

eng

Format of Original

22 p.

Publication Date

10-2004

Publisher

Institute of Electrical and Electronics Engineers (IEEE)

Source Publication

IEEE Transactions on Software Engineering

Source ISSN

0098-5589

Original Item ID

doi: 10.1109/TSE.2004.64

Abstract

Real-time, reactive, and embedded systems are increasingly used throughout society (e.g., flight control, railway signaling, vehicle management, medical devices, and many others). For real-time, interrupt-driven software, timely interrupt handling is part of correctness. It is vital for software verification in such systems to check that all specified deadlines for interrupt handling are met. Such verification is a daunting task because of the large number of different possible interrupt arrival scenarios. For example, for a Z86-based microcontroller, there can be up to six interrupt sources and each interrupt can arrive during any clock cycle. Verification of such systems has traditionally relied upon lengthy and tedious testing; even under the best of circumstances, testing is likely to cover only a fraction of the state space in interrupt-driven systems. This paper presents the Zilog architecture resource bounding infrastructure (ZARBI), a tool for deadline analysis of interrupt-driven Z86-based software. The main idea is to use static analysis to significantly decrease the required testing effort by automatically identifying and isolating the segments of code that need the most testing. Our tool combines multiresolution static analysis and testing oracles in such a way that only the oracles need to be verified by testing. Each oracle specifies the worst-case execution time from one program point to another, which is then used by the static analysis to improve precision. For six commercial microcontroller systems, our experiments show that a moderate number of testing oracles are sufficient to do precise deadline analysis.

Comments

Accepted version. IEEE Transactions on Software Engineering, Vol. 30, No. 10 (October 2004): 634-655. DOI. © 2004 The Institute of Electrical and Electronics Engineers. Used with permission.

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

Download
ahamed_7746acc.docx (766 kB)
ADA Accessible Version

Share

COinS