实时系统的虚拟内存技术

本文对实时系统的虚拟内存技术作了深入的分析和讨论,并以X86处理器为例．在嵌入式操作系统CRTOSII上完成了一个内存管理系统的详细设计与实现。     

实时系统的形式化验证

实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。     

Verification of Real-Time Systems using Linear Relation Analysis

Linear Relation Analysis [11] is an abstract interpretation devoted to the automatic discovery of invariant linear inequalities among numerical variables of a program. In this paper, we apply such an analysis to the verification of quantitative time properties of two kinds of systems: synchronous programs and linear hybrid systems.     

带有时钟变量的线性时序逻辑与实时系统验证

为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.     

Translation and Optimization in the Verification of Real-Time Systems

Compilation or translation is not only an issue at the level of program but also at the level of specification. This talk considers the design of real-time software for Programmable Logic Controllers (PLCs) and discusses questions of correctness and optimization for translations between different semantic models. The need for such translations arises in order to bridge the gap between conceptually clear models on the one hand and computationally feasible models on the other hand.To exemplify this, the talk considers so-called Constraint Diagrams as formalizations of behavioural requirements and so-called PLC-Automata as design specifications. Both Constraint Diagrams and PLC-Automata are given a formal semantics in the Duration Calculus, a logic for real-time systems. To enable an automatic verification (model-checking) of designs against requirements, translations of Constraint Diagrams and PLC-Automata into Timed Automata are presented. Semantic correctness and optimization of these translations are discussed.The concepts presented in the talk are implemented in a tool called Moby-RT that besides the above verification facilities also offers a compiler for PLC code generation.     

一类并发实时系统的自动验证

一个被广泛用于验证实时系统的方法是根据被验证的实时性质,使用适当的双向模拟等价关系使无限的状态空间转化为有限的状态等价类空间.算法只需要在这个有限的等价类空间里搜索就可以得到正确答案.但是,这个等价类空间的规模一般随着系统规模的增大而产生爆炸性的增长,以至于在很多情况下,穷尽搜索这个空间是不现实的.该文引入了一个等价关系来验证一个由多个实时自动机通过共享变量组成的并发系统是否满足一个线性时段特性.同时,还引入了格局之间的兼容关系来避免对状态等价类空间的穷尽搜索.基于这两个关系,文章提出了一个算法来验证是否一个实时自动机网满足一个线性时段特性.实例研究显示,此算法在某些情况下比其他一些工具有更好的时间和空间效率.     

分布实时系统的概率规范和证明形式化

1引言 随着数字系统变得越来越小、越来越便宜,它们用于物理过程控制和与物理过程互协作的机会将越来越多。互相协作的过程如果出现意外行为,后果将可能很严重。这种意外为不仅仅指程序和数字     

分布式实时系统双工容错技术研究

本文介绍一个高可用性的分布式实时双工系统。文中首先建立了系统模型,通过模型给出了系统高可用性的定量公式,最后着重介绍了实现双工的几种主要技术,包括机组切换、数据恢复和双工结果处理等。     

四种嵌入式实时操作系统关键技术分析

介绍了RT-Linux,μCLinux,μC/OS-Ⅱ和eCos四种源码公开的嵌入式实时操作系统（Embedded RealTime Operating Systems,ERTOS）,详细分析比较了关键实现技术——任务管理、任务及中断间的同步通信机制、存储器管理、中断管理等,指出了不同应用领域所适合的ERTOS。     

Rewriting-Based Techniques for Runtime Verification

Techniques for efficiently evaluating future time Linear Temporal Logic (abbreviated LTL) formulae on finite execution traces are presented. While the standard models of LTL are infinite traces, finite traces appear naturally when testing and/or monitoring real applications that only run for limited time periods. A finite trace variant of LTL is formally defined, together with an immediate executable semantics which turns out to be quite inefficient if used directly, via rewriting, as a monitoring procedure. Then three algorithms are investigated. First, a simple synthesis algorithm for monitors based on dynamic programming is presented; despite the efficiency of the generated monitors, they unfortunately need to analyze the trace backwards, thus making them unusable in most practical situations. To circumvent this problem, two rewriting-based practical algorithms are further investigated, one using rewriting directly as a means for online monitoring, and the other using rewriting to generate automata-like monitors, called binary transition tree finite state machines (and abbreviated BTT-FSMs). Both rewriting algorithms are implemented in Maude, an executable specification language based on a very efficient implementation of term rewriting. The first rewriting algorithm essentially consists of a set of equations establishing an executable semantics of LTL, using a simple formula transforming approach. This algorithm is further improved to build automata on-the-fly via caching and reuse of rewrites (called memoization), resulting in a very efficient and small Maude program that can be used to monitor program executions. The second rewriting algorithm builds on the first one and synthesizes provably minimal BTT-FSMs from LTL formulae, which can then be used to analyze execution traces online without the need for a rewriting system. The presented work is part of an ambitious runtime verification and monitoring project at NASA Ames, called PathExplorer, and demonstrates that rewriting can be a tractable and attractive means for experimenting and implementing logics for program monitoring.Supported in part by joint NSF/NASA grant CCR-0234524.     

Low-Power Design for Real-Time Systems

Real-time Systems often are located in the special environments where the power consumption is a big concern. Upon presence of timing constraints, the low power design on the real-time systems has significant impact on the performance as well as the schedulability of the systems. The system developers are facing the challenges for reducing the power consumption and meeting the timing constraints in the real-time systems.This paper represents one of few attempts to address the issue of the low power design on real-time systems. We present two power reduction methods: one is at the software compilation level and the other at the operating system level. Given a real-time program, an inter-instruction power reduction technique is proposed to transform the program to another one with lower power consumption. In addition, a scheduling algorithm for real-time operating systems is proposed to reschedule real-time programs when the execution time of the programs is changed. Therefore, the proposed scheduling algorithm works together with the proposed power reduction technique to make sure all programs meet their deadlines and to improve the system schedulability. We also evaluate the performance of the proposed inter-instruction reduction method by comparing it with the cold scheduling algorithm and show that the proposed method outperforms the cold scheduling algorithm and reduces more energy power.     

μClinux实时改造技术

本文提出了一种对μClinux进行实时改造的方案，该方案采用双内核机制，借助RTLinux的实现思想，利用内核模块的可动态加载技术，对普通μClinux进行实时性改造。实验表明，该系统实时任务的调度响应和中断延时在微秒级别，能够满足硬实时系统对时间的限制。     

安全协议中的形式化验证技术

伴随着网络和通信的迅速发展,安全已经成为一个备受关注的问题,为确保不同系统的安全,出现了许多的安全协议.文中描述了安全协议验证的形式化需求,并且详细阐述了目前流行的几种形式化的验证技术及各自的优缺点,探讨了形式化验证技术所面临的挑战,指出目前在这方面所做的工作以及有待发展的方向.     

安全协议中的形式化验证技术

伴随着网络和通信的迅速发展，安全已经成为一个备受关注的问题，为确保不同系统的安全，出现了许多的安全协议。文中描述了安全协议验证的形式化需求，并且详细阐述了目前流行的几种形式化的验证技术及各自的优缺点，探讨了形式化验证技术所面临的挑战，指出目前在这方面所做的工作以及有待发展的方向。     

Analysis of Checkpointing for Real-Time Systems

Predictable performance in the event of failuresis of paramount importance in most safety critical real-timesystems. Various hardware as well as software fault-toleranttechniques are employed towards this goal among which checkpointingis a relatively cost-effective scheme. Since checkpointing schemesdepend on time redundancy, they could affect the correctnessof the system by causing deadlines to be missed. This paper providesexact schedulability tests for fault tolerant task sets undera specified failure hypothesis and employing checkpointing toassist in fault recovery. The effects of checkpointing strategieson task response time are analysed and some insights for optimalcheckpointing are provided. The emphasis here is on utilizingthis analysis as an off-line design support tool.     

实时产生式系统

产生式系统是一种重要的人工智能程序设计语言,但却比较难于应用到实时领域之中.本文在分析其在实时应用方面两个主要不足的基础上,对实现实时产生式系统的几种可能途径与方法做了较为深入的探讨.