ITR: Static Timing of Interrupt-Driven Software

点击翻译按钮获取中文摘要

ABSTRACTProposal #01122628Purdue Research Palsberg,JensStatic Timing of Interrupt-driven SoftwareReal-time, reactive and embedded systems are widely and increasingly used throughout society (e.g., flight control, railway signaling, vehicle management systems, medical devices). This trend is likely to continue, as applications that would have been unthinkable only a few short years ago come into the reach of ever more complex processors. Many such applications are long lived, interact with their environment continuously, and are under important real-time constraints. As these reactive systems permeate our lives, bringing us everything from intelligent pace-makers to tiny freshness-tracking devices in groceries, the need for cost-effective, confidence-inspiring software validation techniques grows proportionately. This project focuses on building new tools for checking a common class of reactive real-time systems known as interrupt-driven systems. This proposed research has four facets that complement and support each other. The first continues our preliminary work on analyzing seven commercial microcontrollers to identify a static timing analysis that is sufficiently precise for a single interrupt handler. Second, ways of specifying and checking timing properties for multiple interrupt handlers are being investigated. Third, a typed assembly language is being developed with time bounds in which timing properties can be specified in a modular way, one handler at a time. Fourth, a timed interrupt-handler calculus is being designed that will embody our results in a language-independent way and make it tractable to prove key properties. The new tools will automatically derive a model of the software by static analysis and type checking, and submit the result to a model checker. The tools can lead to significantly reduced testing requirements, and provide support for maintenance throughout the systemlife-cycle.