基于混合搜索的含逻辑“与”“或”的RM优化算法

相对于标准约束优化问题,广义约束优化问题（或称析取优化问题）的等式或不等式约束条件中不仅包含逻辑“与”关系,还含有逻辑“或”关系.单调速率（RM）优化问题是广义约束优化问题的一个重要应用.目前RM优化问题已有的解法包括函数变换、混合整数规划、线性规划搜索等算法.随着任务数的增多,这些算法的求解时间较长.提出一种基于线性规划的深度广度混合搜索算法（LPHS）,将广义约束优化问题拆分成若干子问题,建立线性规划搜索树,合理选择搜索顺序,利用动态剪枝算法减小子问题的规模,最终求得最优解.实验结果表明,LPHS算法比其他方法有明显的效率提升.研究成果与计算机基础理论中的可满足性模理论的研究相结合,有助于提高可满足性模理论问题的求解效率,促进该理论在程序验证、符号执行等领域的进一步应用.     

改进的单调速率调度算法

实时系统中调度算法起着重要的作用.单调速率调度算法(rate monotonic algorithm,RM)是一种被 广泛使用的调度算法,并且已被证明是一种最佳的静态优先级算法.传统的RM算法忽略上下文切换需要消耗的时间,针对此问题,提出了一种延迟抢占的改进方法.该方法考虑了上下文切换消耗时间对调度算法的影响,可以减少...     

多处理器单调速率任务分配算法性能评价

多处理器任务分配调度算法是一类经典实时调度算法,然而目前研究在如何根据任务集特征选择任务分配算法方面少见指导性原则,不利于提高多处理器任务分配算法的可调度率及使用尽可能少的处理器达到最优调度结果。基于两种多处理器任务调度策略的比较,本文给出划分策略下的多处理器RM调度的可调度条件和任务分配算法夏分析。仿真结果表明,各任务分配算法所需处理器数与任务集总利用率成正比。同时,分析总结出各算法适用范围及如何根据任务集利用率选择合适算法的指导原则。最后结果还表明,实际算法性能与理论性能界存在差异。     

基于命题投影时序逻辑的单调速率调度算法模型检测

提出了基于命题投影时序逻辑(propositional projection temporal logic,简称PPTL)的单调速率调度(rate monotonic scheduling,简称RMS)模型检测方法.该方法使用SPIN模型检测器的系统建模语言PROMELA为任务调度系统建模,使用PPTL描述系统期望的性质,通过SPIN验证系统模型是否满足性质,从而得知一个任务组在RMS下是否可调度.同时,RMS算法控制下的任务调度系统的其他性质也可以得到验证.     

单调速率任务分配算法利用率的界限分析

通过对单调速率任务分配算法调度策略和可调度条件的分析,在多处理器周期任务抢占调度模型基础上,细致刻画了任务分配算法如何分配任务的行为。依据Liu和Layland定理,给出多处理器下任务分配算法的最小RM利用率界的定理。仿真结果表明,分配算法的利用率界是不同特征任务集选择不同分配算法进行任务划分的关键,通过对任务集总利用率与算法利用率界的比较,判断使用该算法对任务集是否可以产生可行分配。     

基于单调速率的可调度性判定改进算法

在单调速率调度策略的基础上,提出一种改进的任务集可调度性判定算法。该算法通过设定时钟变量模拟调度过程中的系统时钟,在时钟变量值增长过程中,根据任务优先级从高到低的顺序,分析各个任务的截止时间限的满足情况,判定任务的可调度性,从而确定任务集的可调度性。通过实例分析及与现有判定方法的比较,验证了该算法的正确性和高效性。     

基于线性规划的RTL可满足性求解和性质检验

采用线性规划作为基本工具开发一个RTL可满足性求解器,并将其应用于解决RTL性质检验问题．深入研究了使用线性规划约束对RTL电路元器件的建模方法,得到了一种对RTL电路建模的通用方法．通过将RTL性质转化为虚拟RTL电路,找到了一种验证RTL性质的方法．通过实验,并与采用zchaff布尔可满足性求解器的模型检验工具NuSMV进行比较,证明了基于RTL可满足性求解器的性质验证方法在内存和时间消耗上具有相当大的优势．     

混合实时事务的延期单调速率调度算法及其可调度性分析

对于含有实时和非实时两部分的混合实时应用,传统的单调速率调度算法(RM)已不再适用.为此,该文引入“混合实时事务”的概念,并针对这类事务提出一种延期单调速率调度算法(DRM);着重分析了DRM算法对混合实时事务的可调度性;进行了实验测试与性能分析比较．结果表明,事务集中混合实时事务占的比例越高,混合事务中非实时子事务占的比例越大,该算法的CPU使用率阈值就越高,且在各种情况下,DRM算法与RM算法相比性能都更优,最低情况也与之一样．     

基于线性规划的配方优化模型研究

为了解决养殖业饲料配方的优化问题,即在保证饲养原料的用量要求和营养元素的摄入量要求的前提下,使得饲养成本最低。提出了一套完整的转化规则,能够将配方优化问题转化为线性规划数学模型的标准形式,并且在转化过程中能够同时得到初始的基变量和基可行解。最后给出了基于“两阶段法”的优化算法,能够求出每一种饲养原料的正确用量。基于该算法的饲料配方软件已开发成功,通过在南京某乳品公司的实施,证明了该算法的可靠性和实用性。     

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

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

SMT求解器理论组合技术研究

可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎.理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景.因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术.通过对照实验,评估...     

基于多核ARM的数控系统实时性研究

随着数控系统的不断发展,数控系统对精度和速度有了更高的要求,这都对当前普遍采用的单核处理器平台提出了严峻的挑战.基于同构的四核ARM处理器平台,在添加了实时补丁的Linux系统环境下,根据数控系统中硬实时任务、软实时任务、非实时任务并存的特点,把数控系统任务合理的分配到多核ARM上运行,并采用改进的RM算法进行调度,最后对新的任务调度算法进行实时性能测试.本调度模型能够解决了数控系统混合任务调度的问题,并能满足数控系统对实时性的要求.     

一种面向嵌入式实时系统的安全策略优化生成方法

由于受到系统资源和实时性的限制,对于嵌入式实时系统的安全扩展很难延用通用计算机系统的安全设计方法,因此需要对其进行专门的研究。为了在确保实时性的前提下使嵌入式实时系统的安全性达到最优,本文提出了一套完整的安全设计方法,包括安全任务图模型和安全评估模型,在此基础上,又提出了一种基于整数线性规划的安全策略优化生成方法ILPOS。该安全策略优化生成方法同时解决了安全算法选择和实时可调度性检测两方面的问题,克服了一般分阶段优化方法的不足,从而充分地利用系统可用时间来实现安全扩展。仿真实验结果表明,与传统的启发式安全设计算法相比,ILPOS方法在各种实时性约束条件下都能有效地提高系统的安全性。     

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005)

The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.     

利用SMT约束分解方法求解RTL可满足性问题

随着集成电路技术与工艺的不断发展, 目前工业界所采用的形式验证工具已很难适应集成电路规模的飞速增长.为了对RTL电路的可满足性问题进行形式验证, 提出基于超图划分的约束分解实现可满足性模理论 (SMT) 求解的分级验证方法.通过分析RTL电路的结构约束, 对约束集合中的元素和相关变量进行约束建模, 并构建带有合适权重的超图模型;利用超图划分的机制寻找带有最小割集的等量划分, 实现约束分解, 完成RTL电路的定界模型检验.实验结果表明, 该方法能够减小处理问题的规模和求解过程中的搜索空间, 提高验证效率.     

Combining SAT Methods with Non-Clausal Decision Heuristics

A decision procedure for arbitrary first-order formulas can be viewed as combining a propositional search with a decision procedure for conjunctions of first-order literals, so Boolean SAT methods can be used for the propositional search in order to improve the performance of the overall decision procedure. We show how to combine some Boolean SAT methods with non-clausal heuristics developed for first-order decision procedures. The combination of methods leads to a smaller number of decisions than either method alone.     

RTL验证中的混合可满足性求解

RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.