中断驱动系统模型检验

针对一类中断驱动系统提出了一种建模和模型检验的方法.该系统通常由中断处理程序和操作系统调度的任务组成,前者由中断源触发后处理中断事件,后者则负责处理系统的日常任务以及某些中断处理事件的后续处理.因为这类系统是实时控制系统,对中断事件的处理需要在规定时间内响应并完成,否则可能造成严重的系统失效.为了帮助系统设计人员在系统设计过程中应用模型检验技术来提高系统的正确性,首先确定了此类系统中与时序性质相关的系统要素(包括系统调度任务、中断源、中断处理程序)和相关参数,并要求设计人员在设计阶段明确指出这些要素的参数.然后,提出了将这些要素和参数自动转化为形式化模型的方法:使用时间自动机对中断事件进行建模,使用中断向量表和CPU处理栈对中断处理过程进行建模.对于得到的形式化模型,给出了针对中断处理超时错误的检测方法,并在此基础上给出了针对共享资源的完整性、子程序原子性的检验方法.     

嵌入式Forth操作系统实时调度算法研究

针对目前嵌入式Forth操作系统中缺乏实时调度机制的问题,对基于Forth虚拟机架构的嵌入式操作系统中多任务调度的关键技术进行了研究。采用Forth虚拟机技术,新定义了一种中断任务类型来处理实时突发事件,并给出了一种新的任务调度算法来调度 Forth系统中终端任务、后台任务以及中断任务顺利运行。实验结果表明,改进后的 Forth 系统能够通过实时调度处理突发事件,并且实时响应度高,尤其适用于对实时性有要求的嵌入式环境中,以满足日趋复杂的嵌入式环境对高效操作系统和 Forth 技术的应用需求。     

嵌入式操作系统混合任务调度技术与策略研究

针对当前嵌入式系统中时间触发与事件触发混合任务的特点,以μC/OS-II操作系统架构为基础,设计了一种能够同时支持时间触发与事件触发的混合操作系统内核架构。该架构符合OSEK/VDX标准,具有良好的可移植性。针对混合任务调度问题,提出了一种静态周期性可抢占式混合任务调度策略,该策略同时支持中断级与任务级的任务切换,并采用EDF（最早截止时间优先）算法对被抢占的时间触发任务进行恢复,相比OSEKtime OS只能在中断级进行任务切换以及FIFO（先进先出）恢复算法,能够提高系统资源利用率,并最大限度保证任务实时性。实验分析结果表明,所设计的混合操作系统架构移植方便,所提出的混合任务调度策略可行有效,调度过程具有良好的可预测性。     

基于Forth虚拟机的嵌入式多核任务调度研究

由于传统多核任务调度系统对于突发事件的处理,都是基于CPU进行调度的,严重影响了操作系统中任务切换的实时性.于是提出一种基于Forth虚拟机架构的嵌入式多核任务调度系统.为了保证Forth操作系统兼容轮询调度,根据突发事件创建中断任务,并与相应的任务执行程序建立连接.依据中断、终端和后台三种任务间的关联构建循环链表.最后,当突发事件触发中断任务就绪后,Forth系统将调度中断任务去执行突发事件,当中断任务程序运行完毕后,系统继续执行当前任务,执行到原语pause时,当前任务的用户变量将寻找下一任务的TCB首地址,直到所有任务执行完毕.实验结果表明,改进后的Forth虚拟机操作系统响应速度良好,不受任务数量影响,且系统等待时间明显降低,说明所设计的Forth虚拟机操作系统具有良好的多核任务调度性能.     

Linux下中断方式的设备驱动程序设计

中断处理是嵌入式Hnux操作系统的核心任务之一,提高应用程序效率的关键技术是在设备驱动程序中使用中断方式.本文介绍了ARM Linux中断处理过程,研究了Linux下设备驱动程序及其中断服务程序的开发方法和技巧,并实例介绍了键盘中断的服务程序开发方法.     

偶发实时系统可调度性分析问题的整数规划方法

偶发实时任务最早截止期优先（earliest deadline first,简称EDF）可调度分析是实时系统领域经典的NP困难问题.现有的伪多项式时间判定算法（pseudo-polynomail time decision algorithm,简称PTDA）均局限于利用率U严格小于1的同步任务系统.对于U≤1的同步系统或更加困难的异步系统,现有PTDA则不再适用.针对以上问题,为同步和异步两类实时系统建立了统一的整数规划模型,其规模并不依赖于利用率U的取值.基于多面体理论证明了模型维数和极大诱导不等式,进而提出了同/异步系统上EDF可调度性分析问题统一的多项式时间线性松弛求解方法.实验结果表明,该方法能够获得较紧的问题解下界,在异步和同步系统中,线性松弛解与最优解之间的平均百分界差gap分别为0.78%和1.27%.另外,随机生成了大量同步和异步系统的算例,用于该算法和传统算法进行性能比较.对于同步算例,实验结果表明,在U>0.99时,该算法能够对70%的算例给出判定结果,算法性能与QPA算法相比有指数级提升.对于异步算例,实验结果表明,该算法能够对近96%的算例给出可调度性判定.与传统算法相比,该方法将不能判定可调度性的算例比例平均降低了29.27%.对于剩余的4%的算例,该算法将可调度上界的值平均降低了近10⁴倍.     

μC/OS-II中任务调度算法的改进

介绍μC/OS-II嵌入式实时操作系统的特点,分析单一的基于优先级调度算法存在的不足.根据嵌入式应用不同的实时性要求,将应用划分为实时任务、分时任务和后台任务三种类型.针对分时任务,新增加时间片调度算法,给出调度算法的实现方法,同时增加任务创建和销毁的接口;降低基于μC/OS-II操作系统的嵌入式产品开发难度和设计成本,有利于该操作系统的应用推广.     

一种时间触发的多任务调度器设计

复杂的嵌入式系统中,采用传统的前后台单任务控制机制已经不能满足要求。本文在详细分析了时间触发和事件触发模式的优缺点的基础上,设计了一种基于时间触发的多任务调度器;实现了调度器的消息处理机制,并给出了设置硬件定时器的示例代码和周期性任务的处理代码;使用NEC公司的V850平台实现了该调度器,并给出了将该调度器应用于车载音响系统中的模块划分方式和周期性任务的处理方式。     

基于PTIDES执行策略的调度算法

分析现有PTIDES执行策略调度算法,综合考虑事件的截止期和执行时间,改进传统最小空闲时间优先算法,将空闲时间作为事件调度优先权,提出零空闲时间优先PTIDES调度算法——ZSFPTIDES。实例分析表明,ZSFPTIDES调度算法能避免事件在处理过程中因得不到及时处理而夭折的现象,减小事件的抢占切换率,优化分布实时嵌入式系统的调度性能。     

RMX86操作系统应用<之三>

iRX86操作系统中断管理中断和中断处理是实时操作系统的核心。中断是由外部异步产生的事件触发的。通过中断隐含着相应的处理程序来为其服务。对于RMX86系统来讲,其中断管理也不外乎中断一中断向量一中断处理这一系列概念,但也有其特殊点,即中断任务这一概念的引入和使用。一、中断控制器和中断级: RMX86操作系统的中断管理必须借助于一个硬件中断控制器PIC的支持。在iAPX系统中通用的PIC是8259A或80130部件,它们可以支持八个外部中断源,或通过级连从PIC可扩展的64个中断。当RMx86系统处理这些主级或从级中断时,有一些限制,例如系统时钟中断必须接在主级PIC上。又例如若系统中接有NPX,则必须接在主级PIC的0级上。     

Real-time interrupt handling in Ada

The Ada? programming language defines the semantics of interrupt handling as part of the tasking mechanism, making it possible to construct implementation-independent interrupt handlers. However, for the Ada mechanism to be effective, an implementation must provide support not specified by the Ada standard, such as for initializing hardware interrupting devices, handling unexpected interrupts and optimizing for real-time performance constraints. This paper analyses some of the constraints that efficient interrupt support places on an implementation. It develops a model for the interaction between interrupt hardware and Ada tasks and describes optimizations for Ada interrupt handlers. Implementation issues, including task priorities and task termination for interrupt handlers, are discussed in detail.     

航天嵌入式软件整数溢出的形式化验证方法

整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约简技术;同时,针对中断驱动型程序,结合中断函数特征抽象,提出了基于干扰变量的中断驱动程序顺序化方法.经过基准测试程序和真实航天嵌入式软件实验,结果表明：该方法在保证整数溢出问题检出率的前提下,不仅能够提高分析效率,还使得已有的模型检测技术能够适用于中断驱动型程序整数溢出检测.     

一种嵌套中断系统的建模和分析方法

在嵌入式系统和各类操作系统中,中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中,往往会有更紧迫的中断事件请求响应,因而发生中断嵌套.建模并验证嵌套中断系统是一个具有挑战性的工作.本文提出一种建模和验证嵌套中断系统的方法.首先,为中断系统提出了基于投影时序逻辑的定义,并将这种定义推广到包含任意多中断事件的中断系统上,从而得出嵌套中断系统基于投影时序逻辑的形式化模型.其次,使用投影时序逻辑定义的基本中断语句扩充建模仿真和验证语言（MSVL）并扩展MSVL语言的解释器使其可以对嵌套中断系统进行建模仿真和验证.最后通过一个实例展现本文所提出的方法的正确性和实用性.     

Stack size analysis for interrupt-driven programs

We study the problem of determining stack boundedness and the exact maximum stack size for three classes of interrupt-driven programs. Interrupt-driven programs are used in many real-time applications that require responsive interrupt handling. In order to ensure responsiveness, programmers often enable interrupt processing in the body of lower-priority interrupt handlers. In such programs a programming error can allow interrupt handlers to be interrupted in a cyclic fashion to lead to an unbounded stack, causing the system to crash. For a restricted class of interrupt-driven programs, we show that there is a polynomial-time procedure to check stack boundedness, while determining the exact maximum stack size is PSPACE-complete. For a larger class of programs, the two problems are both PSPACE-complete, and for the largest class of programs we consider, the two problems are PSPACE-hard and can be solved in exponential time. While the complexities are high, our algorithms are exponential only in the number of handlers, and polynomial in the size of the program.     

Interrupt Verification via Thread Verification

Most of the research effort towards verification of concurrent software has focused on multithreaded code. On the other hand, concurrency in low-end embedded systems is predominantly based on interrupts. Low-end embedded systems are ubiquitous in safety-critical applications such as those supporting transportation and medical automation; their verification is important. Although interrupts are superficially similar to threads, there are subtle semantic differences between the two abstractions. This paper compares and contrasts threads and interrupts from the point of view of verifying the absence of race conditions. We identify a small set of extensions that permit thread verification tools to also verify interrupt-driven software, and we present examples of source-to-source transformations that turn interrupt-driven code into semantically equivalent thread-based code that can be checked by a thread verifier. Finally, we demonstrate a proof-of-concept program transformation tool that converts interrupt-driven sensor network applications into multithreaded code, and we use an existing tool to find race conditions in these applications.     

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads

Hardware interrupts are widely used in the world’s critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. Handling interrupts properly is an essential component of low-level system programming. Unfortunately, interrupts are also extremely hard to reason about: they dramatically alter the program control flow and complicate the invariants in low-level concurrent code (e.g., implementation of synchronization primitives). Existing formal verification techniques—including Hoare logic, typed assembly language, concurrent separation logic, and the assume-guarantee method—have consistently ignored the issues of interrupts; this severely limits the applicability and power of today’s program verification systems. In this paper we present a novel Hoare-logic-like framework for certifying low-level system programs involving both hardware interrupts and preemptive threads. We show that enabling and disabling interrupts can be formalized precisely using simple ownership-transfer semantics, and the same technique also extends to the concurrent setting. By carefully reasoning about the interaction among interrupt handlers, context switching, and synchronization libraries, we are able to—for the first time—successfully certify a preemptive thread implementation and a large number of common synchronization primitives. Our work provides a foundation for reasoning about interrupt-based kernel programs and makes an important advance toward building fully certified operating system kernels and hypervisors.     

Deadline analysis of interrupt-driven software

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.     

Synchronous and asynchronous handling of abnormal events in the μsystem

This paper presents a general model for dealing with abnormal events during program execution and describes how this model is implemented in the μSystem. (The μSystem is a library of C definitions that provide light-weight concurrency on uniprocessor and multiprocessor computers running the UNIX operating system.) Two different techniques can be used to deal with an abnormal event: an exception, which results in an exceptional change in control flow from the point of the abnormal event; and an intervention, which is a routine call from the point of the abnormal event that performs some corrective action. Users can define named exceptions and interventions in conjunction with ones defined by the μSystem. Exception handlers and intervention routines for dealing with abnormal events can be defined/installed at any point in a program. An exception or intervention can then be raised or called, passing data about the abnormal event and returning results for interventions. Interventions can also be activated in other tasks, like a UNIX signal. Such asynchronous interventions may interrupt a task's execution and invoke the specified intervention routine. Asynchronous interventions are found to be useful to get another task's attention when it is not listening through the synchronous communication mechanism.     

On software verification for sensor nodes

We consider software written for networked, wireless sensor nodes, and specialize software verification techniques for standard C programs in order to locate programming errors in sensor applications before the software's deployment on motes. Ensuring the reliability of sensor applications is challenging: low-level, interrupt-driven code runs without memory protection in dynamic environments. The difficulties lie with (i) being able to automatically extract standard C models out of the particular flavours of embedded C used in sensor programming solutions, and (ii) decreasing the resulting program's state space to a degree that allows practical verification times.We contribute a platform-dependent, OS-independent software verification tool for OS-wide programs written in MSP430 embedded C with asynchronous hardware interrupts. Our tool automatically translates the program into standard C by modelling the MCU's memory map and direct memory access. To emulate the existence of hardware interrupts, calls to hardware interrupt handlers are added, and their occurrence is minimized with a double strategy: a partial-order reduction technique, and a supplementary reachability check to reduce overapproximation. This decreases the program's state space, while preserving program semantics. Safety specifications are written as C assertions embedded in the code. The resulting sequential program is then passed to CBMC, a bounded software verifier for sequential ANSI C. Besides standard errors (e.g., out-of-bounds arrays, null-pointer dereferences), this tool chain is able to verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals.Verification for wireless sensor network applications is an emerging field of research; thus, as a final note, we survey current research on the topic.