基于交互式马尔可夫链的模型检验

研究了基于交互式马尔可夫链（IMC)的模型检验,IMC是集功能描述和性能刻画为一体的并发系统模型,模型检验是一种自动功能验证与性能评价技术。文中提出的模型检验算法结合了传统的功能验证与性能评价的功能,并且与现有的算法相一致。实验分析表明,该算法具有较高的性能,适用于大型复杂系统的验证和评价。     

一种快速JPEG图像检索方法

给出了一种基于归一化转动惯量（Normalized Moment Inertia,NMI)的JPEG图像快速检索方法,其特点是直接在压缩域中DCT系数进行块分类,每一类分块形成一个直值索引图,统计该索引图的NMI值作为该类的一个特征,所有类的NMI特征构成了图像的一个特征序列,以此进行图像检索。本方法不需要完全解压缩,降低了计算复杂度,对图像的平移,旋转和尺度变换有较好的鲁棒性,试验结果表明这种图像检索方法具有良好的检索性能。     

Moore机表示的系统迭代设计动态CTL模型检验的不变性研究

模型检验是系统级设计中验证可信计算系统安全性性质的有效方法。动态模型检验是模型随设计过程而变化的模型检验,动态模型检验过程中遇到的最严重问题之一是模型变化所带来的重复检验代价太高。因此,寻找不变性以避免重复检验显得尤为重要。不变性是一种贯穿系列模型检验而保值为真的性质。该文构建动态模型检验的形式化框架,进而提出基于Moore机描述的流控制系统迭代设计过程的不变性理论,该系统是一种嵌入式控制系统,在可信通信中用以处理数据转换,最后展示了若干非平凡CTL性质在迭代过程中的可保持性。     

组合电路中逻辑错误诊断方法研究*

介绍了近些年出现的几种错误诊断方法,它们在传统方法的基础上利用启发式对原有方法进行了不同程度的改进和提高,产生了较好的诊断结果.     

负载自适应的异构MPSoC任务调度算法研究

在异构MPSoC中,并行任务通过调度算法被分配到各个处理器核上运行,因而任务调度算法的优劣将直接影响异构MPSoC的应用性能。根据处理器核类型和任务间依赖关系,以减小任务间通信开销为目标,提出一种具备负载自适应能力的异构MPSoC任务调度算法。首先,将待调度任务集划分为多个并行任务子集;其次,在考虑处理器核负载的基础上,根据并行任务子集集合、处理器核集合及任务子集在各个核上的执行效率生成赋权二部图;最后,利用赋权二部图最大权匹配方法,将并行任务子集合理地调度到负载适应的处理器核上运行,以降低任务集的平均调度长度,并提高处理器核利用率,从而实现异构MPSoC应用性能的提升。仿真实验在不同的任务总数、任务最大前驱数、核类型、核数量的应用场景下,通过任务集平均调度长度、处理器核利用率两项指标对提出算法进行了定量分析。结果表明,提出算法能有效降低任务集平均调度长度,在实现负载自适应的同时提高异构MPSoC处理器核的利用率。     

基于线性误差断言的推理方法

误差在系统中是普遍存在的。在安全关键系统中,对误差的定量分析是必要的,而以往的推理验证方法较少考虑误差。误差通常用区间数来刻画,从而推广了线性断言,并给出了线性误差断言的概念。此外,结合凸集的性质,提出了求解线性误差断言顶点的具体方法,并验证了该方法的正确性。通过分析相关概念及定理,将判断线性误差断言之间的蕴含关系的问题转化为前驱断言的顶点是否被包含在后驱断言的零点集的判断问题,从而给出了判断线性误差断言的蕴含关系的具体方法步骤,且该方法易于在计算机上编程实现。最后,给出该方法在火车加速状态上的应用,并且用大量随机实例测试了该方法的正确性。与不含误差语义的推理方法相比,该方法在含误差参数的系统的推理验证领域是有优势的。     

一种负载感知的异构MPSoC任务调度算法

处理器核的异构性、运行时负载和任务间依赖关系,是影响异构MPSoC任务调度算法性能的关键因素。该文提出了一种负载感知的异构MPSoC任务调度算法,在满足任务间依赖关系的前提下,根据计算开销和通信负载将待调度任务集划分为任务子集。在考虑处理器核负载状态的基础上,通过赋权二部图最大权匹配,将任务子集调度到适载的处理器核上运行,提高了待调度任务集总执行效率。仿真实验结果表明,该算法有效降低了任务集的调度长度,提高了处理器核的利用率。     

MPSoC核协调可靠性和性能的形式化验证

为了在早期发现片上多核处理器（MPSoC）设计缺陷,本文提出了一种对核协调进行结构建模和性质刻画的形式化方法。在标记变迁系统中引入多项式函数替代动作表达核协调过程中对数据的改变,加入物理元器件发生故障的概率属性,形成用以描述核协调可靠性和性能的混杂马尔科夫决策过程模型。采用随机时序逻辑刻画系统性质,通过模型检测工具验证分析,以银行数据脱敏MPSoC为例,分析系统可靠性和时间延迟与能耗等性能指标。这些验证结果对于早期MPSoC设计人员具有较强的指导作用。     

线性半代数变迁系统的近似互模拟等价

针对软件程序状态间转移关系存在不等式约束的问题,给出一种形式化的程序描述系统,即线性半代数变迁系统。在该系统的基础上,为简化软件程序结构,采用特征列的方法,提出了基于线性半代数系统共同零点的互模拟等价概念及计算方法。但在工程应用中大多数实验所得数据仅为给定误差范围内的近似值,精确的系统等价关系缺乏容错性及灵活性。为获得更恰当的系统关系,利用奇异值分解对系统进行近似处理,建立了系统的近似互模拟等价概念及计算方法。通过符号与数值混合计算,实现误差可计算及可控制。最终选取近似等价系统代替原复杂系统。并发通信程序中的实例分析表明,该方法在简化软件程序设计中具有合理性及有效性。     

CWA formalizations in multi-valued logics

To enhance the expressive power and the declarative abiltity of a deductive database,various CWA(Closed World Assumption)formalizations including the naive CWA,the generalized CWA and the careful CWA are extended to multi-valued logics.The basic idea is to embed logic formulas into some polynomialring,The extensiona can be applied in a uniform manner to any finitely multi-valued logics,Therefore they also of computational significance.