城市交通中车队状态观测器的一种新算法

本文阐述了离散时间点过程理论,时变马尔科夫链及鞅差分序列在城市交通车队状态观测器中的应用。并在此基础上,改进了[5]中的估计算法。用本文提出的非线性最小方差估计算法,对提供的交通状态进行估计,所得结果比[5]中算法精度有明显提高。在大连市某交通干线计算机控制系统中初步应用,取得了令人满意的结果。

basic research in computer science and software engineering at sklcs

The State Key Laboratory of Computer Science (SKLCS) is committed to basic research in computer science and software engineering. The research topics of the laboratory include: concurrency theory, theory and algorithms for real-time systems, formal specifications based on context-free grammars, semantics of programming languages, model checking, automated reasoning, logic programming, software testing, software process improvement, middleware technology, parallel algorithms and parallel software, computer graphics and human-computer interaction. This paper describes these topics in some detail and summarizes some results obtained in recent years.

时间符号迁移图及其互模拟判定

引入时间符号迁移图的概念，作为既涉及通讯又具有实时性的并发系统的模型。该文给出了这种迁移图时间互模拟的算法，并证明了该算法的正确性。

一种基于时间自动机的实时系统测试方法

基于时间自动机(timedautomata,简称TA)的一种变体——时间安全输入/输出自动机(timedsafetyinput/outputautomata,简称TSIOA),提出了一种实时系统测试方法.该方法首先将时间安全输入/输出自动机描述的系统模型转换为不含抽象时间延迟迁移的稳定符号状态迁移图(untimedstabletransitiongraphofsymbolicstate,简称USTGSS);然后采用基于标号迁移系统(labeledtransitionsystem,简称LTS)的测试方法来静态生成满足各种结构覆盖标准的包含时间延迟变量迁移动作序列;最后,给出了一个根据迁移动作序列构造和执行测试用例的过程,该过程引入了时间延迟变量目标函数,并采用线性约束求解方法动态求解迁移动作序列中的时间延迟变量.

支持SAR系统高分辨率实时成像的实时系统解决方案

随着信息技术的发展 ,用于军事、地理、自然灾害扫描探测的合成孔径雷达系统 (SAR)对其成像能力的分辨率和实时显示要求越来越高 因此 ,研究具有自主知识产权的、可以实时处理高分辨率成像的实时系统迫在眉睫 针对实时数据接收、存储、显示和处理等核心问题 ,提出了一种实时系统解决方案 该方案通过对Linux内核的实时扩展 ,实现了可达到高处理机利用率的多任务实时调度方法 ,可支持混成调度 ;在应用层实现符合实时需求的功能模块 ;为DSP板开发实时驱动 ,形成了从硬件驱动层和操作系统层 ,直到应用软件层的完整实时计算体系

一种改进的RM可调度性判定算法

固定优先级任务可调度性判定是实时系统调度理论研究的核心问题之一.目前已有的各种判定方法可归结为两大类:多项式时间调度判定和确切性判定.多项式时间调度判定通常采用调度充分条件来进行,为此,许多理想条件下基于RM(rate monotonic)调度算法的CPU利用率最小上界被提了出来.确切性判定利用RM调度的充要条件,保证任何任务集均可被判定,并且判定结果是确切的.但是由于时间复杂度较差,确切性判定方法难以实现在线分析.提出了一种改进的RM可调度性判定方法(improved schedulability test algorithm,简称ISTA).首先介绍了任务调度空间这一概念,并提出了二叉树表示,然后进一步提出了相关的剪枝理论.在此基础上,研究了任务之间可调度性的相关性及其对判定任务集可调度性的影响,提出并证明了相关的定理.最后基于提出的定理,给出了一种改进的伪多项式时间可调度性判定算法,并与已有的判定方法进行了比较.仿真结果表明,该算法平均性能作为任务集内任务个数的函数具有显著提高.

单调速率及其扩展算法的可调度性判定

任务可调度性判定是实时系统调度理论研究的核心问题.单调速率(RM)算法是实时调度的重要算法,自其提出以来已被广泛研究.然而到目前为止,尚缺乏专题性的文章来系统而深入地探讨RM及其扩展算法的可调度性判定,以及各种现实条件和实现方式(包括任务调度的时间开销和任务同步问题等)对可调度性的影响.围绕RM算法下的可调度性判定问题,由浅入深,系统性地讨论各种不同假设和实现方式对可调度性的影响,具体分为下述3大类问题:(1)理想的RM算法下的可调度性判定的CPU利用率最小上界及可调度的充分必要条件;(2)考虑调度时间开销情况下的可调度性判定条件;(3)优先级反转协议及其对可调度性的影响.给出了具体实例来阐述上述问题,并从算法复杂度和可检测率两方面来比较各种算法的优劣.

一种静态最少优先级分配算法

随着实时系统越来越多地应用于各种快速更新系统,尤其是各种片上系统,如PDA(personal digital assistant),PSP(play station portable)等,性价比已成为系统设计者的主要关注点.实际应用中,实时系统通常仅支持较少的优先级,常出现系统优先级数小于任务数的情况(称为有限优先级),此时,需将多个任务分配到同一系统优先级,RM(rate monotonic),DM(deadline monotonic)等静态优先级分配算法不再适用.为此,静态有限优先级分配是研究在任务集合静态优先级可调度的情况下,可否以及如何用较少或最少的系统优先级保持任务集合可调度.已有静态有限优先级分配可分为两类:固定数目优先级分配和最少优先级分配.给出了任意截止期模型下任务静态有限优先级可调度的充要条件以及不同静态有限优先级分配间转换时的几个重要性质,指出了系统优先级从低到高分配策略的优越性,定义了饱和任务组与饱和分配的概念,证明了在任务集合静态优先级可调度的情况下,最少优先级分配比固定数目优先级分配更具一般性.最后提出一种最少优先级分配算法LNPA(least-number priority assignment).与现有算法相比,LNPA适用范围更广,且复杂度较低.

基于逻辑"或"约束优化的实时系统设计

标准约束优化问题的等式或不等式约束之间是逻辑“与”关系，目前已经有很多高效、收敛的优化算法．但是，在实际应用中有很多更一般的约束优化问题，其等式或不等式约束之间不仅包含逻辑“与”关系，而且还包含逻辑“或”关系，现有的针对标准约束优化问题的各种算法不再适用，给出一种新的数学变换方法，把具有逻辑“或”关系的不等式约束转换为一组具有逻辑“与”关系的不等式，并应用到实时单调速率调度算法的可调度性判定充要条件中，把实时系统设计表示成混合布尔型整数规划问题，利用经典的分支定界法求解．实验部分指出了各种方法的优缺点．

实时系统开发方法研究

1 引言实时系统不仅要求所产生的结果在逻辑上是正确的,而且要求在时间上也是正确的。它已渗透到了社会生活的各个领域,如在过程控制、敏捷制造、核反应堆、航天航空和电讯业上都发挥了重要作用。对于实时系统来说,它应具备以下几个重要特性: ·及时性;实时系统所产生的结果在时间上有着严格的要求,只有符合时间约束的结果才是正确的。在实

改进的以SMT为基础的实时系统限界模型检测

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.

网络控制系统稳定性的图理论

针对具有有界时延和数据包丢失的网络控制系统,提出了一种新的稳定性判据.基于Lyapunov方法和图论理论,给出非线性离散和连续网络控制系统渐近稳定的充分条件,获得保持这两类系统稳定的最大允许时延界,得到控制器设计方法.并且,利用区间矩阵的谱特征,给出网络控制系统区间稳定的充分条件.设计算法,获得比例积分反馈控制器增益.算例表明所提方法的有效性。

面向实时控制任务的高速数据采集存储方法

提出一种基于CAN总线,面向实时控制任务的高速数据采集存储方法.该方法将数据实时采集、系统实时控制、数据存储与显示分配在相互独立的处理单元中实现,处理单元之间通过独立的CAN网络进行通信.该数据采集方法解决了数据实时采集与系统实时控制之间的矛盾.利用队列技术,该方法解决了数据存储与数据实时显示之间的矛盾.该数据采集存储方法已成功应用到某大型仿真系统中.

机器人机械手的离散时间学习控制

本文为机器人机械手提出了一种基于离散时间的重复学习控制法，这种学习控制法利用机器人动力学模型的部分知识，从它的特性和实用观点看，这种控制法比现有的其它学习控制法更有吸引力．本文还给出了学习控制法的收敛性证明和计算机仿真结果。

A Scheduling Algorithm for Flexible Manufacturing Cell

In this paper, a new scheduling algorithm for the flexible manufacturing cell is presented, which is a discrete time control method with fixed length control period combining with event interruption. At the flow control level we determine simultaneously the production mix and the proportion of parts to be processed through each route. The simulation results for a hypothetical manufacturing cell are presented.