ITR: Static Timing of Interrupt-Driven Software

ITR：中断驱动软件的静态时序

• 批准号: 0401680
• 负责人: Jens Palsberg
• 金额: $ 33.59万
• 依托单位: University of California-Los Angeles
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-09-01 至 2006-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0401680&HistoricalAwards=false
• 关键词: ITR; Static; Timing; Interrupt; Driven

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.

摘要提案 #01122628Purdue Research Palsberg，Jen​​s 中断驱动软件的静态定时实时、反应式和嵌入式系统在整个社会中得到广泛且越来越多的使用（例如，飞行控制、铁路信号、车辆管理系统、医疗设备）。 这种趋势可能会持续下去，因为几年前还无法想象的应用程序已经进入了更加复杂的处理器的范围。 许多此类应用程序的生命周期很长，与环境持续交互，并且受到重要的实时约束。 随着这些反应系统渗透到我们的生活中，给我们带来从智能起搏器到食品杂货中的微型新鲜度跟踪设备的一切，对具有成本效益、令人信心十足的软件验证技术的需求也相应增长。 该项目的重点是构建新工具来检查一类常见的反应式实时系统（称为中断驱动系统）。 这项拟议的研究有四个方面，相互补充和支持。 第一个继续我们分析七个商用微控制器的初步工作，以确定对于单个中断处理程序来说足够精确的静态时序分析。 其次，正在研究指定和检查多个中断处理程序的时序属性的方法。 第三，正在开发一种具有时间限制的类型化汇编语言，其中可以以模块化方式指定定时属性，一次一个处理程序。 第四，正在设计定时中断处理程序演算，它将以独立于语言的方式体现我们的结果，并使其易于证明关键属性。 新工具将通过静态分析和类型检查自动导出软件模型，并将结果提交给模型检查器。 这些工具可以显着降低测试要求，并为整个系统生命周期的维护提供支持。