中断驱动控制系统的有界模型检验技术

针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作.使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模,并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程.控制变量将中断处理过程和系统任务相关联,中断处理程序可以设定某个控制变量,而系统任务则通过检查该控制变量来确定是否需要进行后续处理.对于这样的形式化模型,给出了检验关键时序性质的有界模型检验算法.该算法使用深度优先的方式遍历所有长度小于等于K的可行路径,并使用SMT Z3实现了对时间约束和规约的处理.     

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

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

着色Petri网对高性能集群的建模与性能评估

针对形式化建模方法导致的状态空间爆炸问题,提出了一种基于Petri网的高性能集群建模与性能评估方法.首先分析了高性能集群的系统架构,构建了模型的总体结构;然后针对集群系统建立了相应的任务产生子模型和调度子模型,并通过对Petri网进行着色,根据不同种类任务的执行特点设计了相应的任务处理模型.仿真结果表明,利用所建立的模型能够有效评估关键参数对集群性能的影响.     

基于事件图的离散事件仿真模型并行检验方法

非形式化仿真模型验证方法易受主观因素的影响且具有不完备性,而传统的形式化模型检验方法由于受到状态空间爆炸问题的影响,很难处理大规模的仿真模型.并行模型检验方法以其完备性、高效性已经在工业界中得到了成功的应用,但是由于涉及到形式化规约、逻辑学以及并行计算等多项技术,应用难度较大.针对上述问题,提出了基于事件图的离散事件仿真模型并行检验方法.该方法首先对事件图在模型同步方面进行了扩展,给出了扩展事件图的形式化定义、语法及语义;然后将扩展事件图模型转换到分布并行验证环境的DVE模型,成功地将并行模型检验方法应用于仿真模型验证领域.该方法使得仿真人员无须学习新的形式化验证语言就能采用并行模型检验方法对仿真模型进行形式化验证,可降低模型并行验证的难度,从而有效提高模型验证的效率和完备性.实验结果表明了该方法的有效性,有利于扩展并行模型检验方法在仿真领域中的应用.     

基于SysML的复杂机电系统设计模型形式化扩展与验证

形式化系统验证是保证系统设计正确性的一种重要手段.如何针对复杂机电系统物理与软件相融合的特征,对系统设计的动态特征进行验证,是系统验证研究领域亟待解决的问题.针对这一问题,对系统工程标准建模语言SysML进行扩展,提出了一套形式化系统模型验证方法.首先,以计算树逻辑和基于流的功能表示为形式化基础,形成基于SysML的系统功能建模方法;然后,以混合自动机为基础,建立基于SysML的系统行为建模方法;最后,针对物理与软件子系统的不同动态特征,借助NuSMV模型校验器,以层次化方式实现系统模型的自动验证.以移动机器人系统为例,展示了复杂机电系统设计模型的自动验证过程.     

基于UML的嵌入式系统建模及模型验证机制研究

统一建模语言UML在嵌入式系统设计建模中已经获得了广泛的认可，并有很多成功的应用，但UML存在时间约束描述能力不强和所建模型形式化复杂、验证难的问题。针对上述问题，本文提出了使用UML扩展机制对UML状态图进行时间扩展，建立系统状态一约束一事件矩阵来对模型进行形式化描述的方法。该方法解决了UML在嵌入式系统建模时存在的问题。应用实例和实验结果验证了该方法的可行性和有效性。     

一种基于航电系统架构模型的故障树自动建模方法

航电系统作为安全关键系统,利用故障树对其进行安全性分析十分必要。然而,传统的故障树依靠手工构建,主要依赖于分析人员对系统的理解程度;同时由于安全性分析人员与系统设计人员对系统的理解不同而很难保证失效模式与系统架构的一致性。针对上述问题,提出了一种基于航电系统架构模型的故障树自动建模方法:通过向系统设计模型中添加相应的安全性属性,并嵌入高级形式化语言AltaRica中的断言机制描述故障转移过程,由此形成安全性分析模型;基于此模型利用路径追溯的方法完成故障树自动建模。以某飞机驾驶舱显示系统为案例的研究结果表明,所提出的方法能基于航电系统架构模型有效进行故障树自动建模,从而确保了故障树分析结果的完整性。     

AADL在中断控制系统建模中的应用

随着中断控制在嵌入式实时系统中的不断广泛应用,中断控制的可靠性是系统设计中面临的重要问题。虽然基于体系结构分析与设计语言(AADL)的形式化方法为这一问题的解决提供了思路,但AADL自身缺少 有效的元素和 方法来描述和建模中断。为此,提出一种结合AADL与中断控制器的中断控制系统设计方法,并运用GSPN可靠性计算模型对可靠性进行分析,从而为AADL在航电系统中的应用提供了思路。     

基于时间Petri网的嵌入式系统中断建模与验证

嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上述问题,文中首先提出了一种基于时间Petri网的中断系统建模方法,其能够对中断的并发性和时间序列进行有效建模。然后,为方便后续形式化验证,将时间Petri网模型转化为与之等价的时间自动机模型,并提出一种符号编码方法对时间自动机进行形式化编码,将系统模型与所需验证性质编码为一阶谓词逻辑公式,从而能够通过SMT对时间自动机的不变属性进行BMC验证。最后,通过SMT求解器Z3进行实验,实验结果证明了所提方法的有效性。     

基于UML的嵌入式建模方法改进策略研究

统一建模语言UML(unified modeling language)在嵌入式系统设计建模中已经获得了广泛的承认,有很多成功的应用.但UML在嵌入式建模中存在时间约束描述能力不强和所建模型形式化复杂、验证难及模型重用性不高等问题.针对这些问题提出了一种改进策略:定义实时语义和映射规则,建立实时描述模式模板,使用模板中实时描述模式描述时间约束信息.改进后的方法能可视化地分析模型、纠正错误和简单地进行形式化转换,能利用支撑工具对模型进行验证,较好地解决了UML在嵌入式系统建模中存在的问题.     

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.     

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.     

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.     

Optimal Checkpoint Placement on Real-Time Tasks with Harmonic Periods

This paper presents an optimal checkpoint strategy for fault-tolerance in real-time systems where transient faults occur in Poisson distribution. In our environment, multiple real-time tasks with different deadlines and harmonic periods are scheduled in the system by rate-monotonic algorithm, and checkpoints are inserted at a constant interval in each task. When a fault is detected, the system carries out rollback to the latest checkpoint and re-executes tasks. The maximum number of re-executable checkpoints and an equation to check schedulability are derived, and the optimal number of checkpoints is selected to maximize the probability of completing all the tasks within their deadlines.     

Fault-Tolerant Scheduling for Real-Time Embedded Control Systems

With the increasing complexity of industrial application, an embedded control system (ECS) requires processing a number of hard real-time tasks and needs fault-tolerance to assure high reliability. Considering the characteristics of real-time tasks in ECS, an integrated algorithm is proposed to schedule real-time tasks and to guarantee that all real-time tasks are completed before their deadlines even in the presence of faults. Based on the nonpreemptive critical-section protocol (NCSP), this paper analyzes the blocking time introduced by resource conflicts of relevancy tasks in fault-tolerant multiprocessor systems. An extended schedulability condition is presented to check the assignment feasibility of a given task to a processor. A primary/backup approach and on-line replacement of failed processors are used to tolerate processor failures. The analysis reveals that the integrated algorithm bounds the blocking time, requires limited overhead on the number of processors, and still assures good processor utilization. This is also demonstrated by simulation results. Both analysis and simulation show the effectiveness of the proposed algorithm in ECS.     

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.     

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.     

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.     

Parameter adaptation for generalized multiframe tasks: schedulability analysis,case study,and applications to self-suspending tasks

The generalized multiframe task model (GMF) extends the sporadic task model and multiframe task model. Each frame in the GMF model contains an execution time, a relative deadline, and a minimum inter-arrival time. These parameters are fixed after task specification time in the GMF model. However, multimedia and adaptive control systems may be overloaded and no longer stabilized when the task parameters in such systems are not flexible. In order to address this problem, deadlines and periods of frames may change to alleviate temporal overload, e.g., in the parameter adaptation and elastic scheduling model. In this paper, we propose a new model GMF-PA (the GMF model with parameter adaptation). This model allows task parameters to be flexible in arbitrary-deadline systems. A necessary schedulability test based on mixed-integer linear programming is given to check the schedulability under EDF scheduling and optimally assign frame deadlines and periods at the same time. We also prove that the test is a sufficient and necessary schedulability test when frame deadlines and periods must be integers. An approximation algorithm is also deployed to reduce computational running time and indicates a sufficient schedulability test in general. The speed-up factor of our approximation algorithm is \(1+\epsilon \) where \(\epsilon \) can be arbitrarily small, with respect to the exact schedulability test of GMF-PA tasks under EDF. We also apply the GMF model to self-suspending tasks. By extending recent work on scheduling self-suspending tasks, we remove the assumption that frame deadlines are equally assigned in self-suspending tasks, and the system is extended from constrained-deadline systems to arbitrary-deadline systems. We have done extensive experiments to show that the schedulability ratio is improved using our techniques in our GMF-PA model.