轨道交通联锁领域特定语言的形式化

作为轨道交通系统的核心子系统之一，对联锁系统进行形式化建模与分析，是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合，由于形式化知识难以掌握，领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题，针对联锁系统的故障随机性、行为实时性、构件可重用的特点，提出设计联锁领域特定语言IS-SDL描述具体的联锁系统的参数，并基于随机混成自动机模板自动生成联锁系统的形式化模型，以进一步在此基础上进行安全分析.首先对联锁系统模型进行分析，根据不同案例设计其领域特定语言；其次，确定联锁系统的系统模型的模板，包括环境构件模板和控制器模板，并举例抽取其随机混成自动机模板；在模板基础上定义系统模型生成过程，让领域专家可以通过领域特定语言，输入参数自动生成具体的随机混成自动机系统模型；最后以某站联锁系统为例，展示了基于模板的具体系统模型的生成过程，并通过基于系统模型的事故预测分析，证明了该方法的可行性与有效性.     

多序列比对算法族的形式化设计与生成

多序列比对问题是生物信息学研究的重要部分，是解决物种进化关系、基因组序列分析等问题的基础。多序列比对算法具有很高的专用性，不同的算法适用于不同的研究环境。目前常用的多序列比对软件是在生物信息学理论指导下利用多个子算法装配形成的，而现有的研究主要针对特定算法的特定步骤进行优化，缺乏领域层次高抽象性的算法框架研究，致使多序列比对算法较为繁杂且冗余过多。根据产生式编程以及软件复用的思想，分析了多序列比对算法族MSAA的特征，设计了相应的泛型算法构件并刻画了构件间的交互关系，进一步借助PAR平台形式化构建了MSAA构件库，提高了装配算法的可靠性和组装灵活性，便于研究人员的维护和优化。     

一种基于测量构件变迁模型的可重构测量构件一致性检测方法

可重构网络测量系统中,工作流测量构件间迁移的过程是否与规约描述一致,是检验测量构件一致性测试的重要内容。建立了一种基于工作流的构件变迁模型MCTM(Measurement Component Transfer Model),详细阐述了MCTM模型的形式化定义,并基于MCTM模型给出了一种能自动生成遍历所有构件的测试用例生成算法CTBMCTM。实验结果表明,CTBMCTM算法可以准确定位存在问题的构件,与T&GS算法相比,该算法在生成较短测试序列的同时显著缩短了算法的运行时间。     

基于PAR的算法形式化开发

形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的算法思想,在相关工具的支持下自动生成算法程序.研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动,降低了形式化求解算法问题的难度,提高了算法程序的可靠性和形式化开发效率.     

若干算法程序的形式化推导与生成技术研究

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C 等可执行程序.     

基于问题模式的形式化软件规格说明生成方法

精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明.     

自动术语抽取研究综述

自动术语抽取是从文本集合中自动抽取领域相关的词或短语，是本体构建、文本摘要、知识图谱等领域的关键基础问题和研究热点.特别是，随着近年来对非结构化文本大数据研究的兴起，使得自动术语抽取技术进一步得到学者的广泛关注，取得了较为丰富的研究成果.本文以术语排序算法为主线，对自动术语抽取方法的理论、技术、现状及优缺点进行研究综述：首先概述了自动术语抽取问题的形式化定义和解决框架.然后围绕“浅层语言分析”中基础语言信息和关系结构信息两个层面的特征对近年来国内外的研究成果进行分类，系统总结了现有自动术语抽取方法的研究进展和面临的挑战.最后对术语抽取使用的数据资源及实验评价进行分析，并对自动术语抽取未来可能的研究趋势进行了探讨与展望.     

一种基于线性逻辑的构件组装方法研究

构件组装是基于构件的软件开发中的一个重要环节.本文利用线性逻辑描述了具有语义信息的构件结构,描述了独立于具体的计算环境、具有普遍适用性的三种构件组装关系,利用定理证明的方法,根据现存构件的描述和构件组装关系自动生成构件组装的方案,并从被适应的构件描述中推导出复合构件的描述,以提高对构件适应过程的描述和分析能力,为构件组装形式化分析、组装正确性的检验提供了保证,并列出了一些值得进一步研究的问题.     

接口连接式构件组装的一种形式化方法

构件组装是基于构件的软件开发的研究重点之一，能够有效地提高软件开发的效率和质量。以往大部分构件组装技术是在“成功组装路线”的前提条件下实现的，缺乏对构件组装正确性的检验。本文改进了常用的接口连接式构件组装技术，采用形式化方法描述和推导与构件以及构件组装相关的问题，给出了映射算法，实现了从构件组装规约向粘合代码的自动转换，为构件组装形式化分析、组装正确性检验提供了保证。     

Radl算法到Apla程序的生成系统

算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率.     

Modelica建模软件中拓扑排序相关算法研究

为了提高现有OpenModelica软件对DAE系统的预处理模块中求强连通分量与拓扑排序部分的性能,提出了基于Kosaraju算法实现的策略.阐述了Modelica软件的实现原理,叙述了拓扑排序相关算法在其中的重要性,分析了现有Modelica 软件中使用的求强连通分量与拓扑排序部分的算法,比较了Tarjan算法的实现方案与Kosaraju算法实现方案.对两种方案进行了比较和分析结果,表明了Kosaraju算法方案的可行性和有效性.     

一种新型单循环排序算法

排序是计算机程序设计中一项经常而又重要的操作,研究排序算法具有重要的理论意义和广泛的应用价值。通过对目前常用的几种排序算法的研究,指出它们均为双重循环或多重循环结构设计,借鉴了军队排队列的思想,提出一种只需要单重循环结构即可完成排序过程的新型算法,并进行了编程实现。通过对该算法的时间复杂度、空间复杂度以及稳定性等性能分析,证明该算法对于基本有序的数据排列排序性能优秀,对于数据排列大都是两两错位的排序过程接近最优算法。     

利用帕累托非支配关系实现高效三目标差分进化的方法

在多目标进化算法中,时间复杂度过高是普遍的问题,特别是三个目标函数以上时,解的等级分配占用了过多运算时间。针对三目标问题,利用帕累托支配关系,对解的等级分配进行研究,发现经典的等级排序及分配方法存在一定冗余操作,需对全部的解先排序后,才能再分配等级并选择下一代,造成部分不必要的运算。为减少该冗余,利用帕累托非支配关系结合差分进化,实现高效三目标进化算法。算法每次迭代对种群中最高等级的个体进行计算,在分配等级同时进行选择后代个体操作,当后代种群生成时便跳出计算,从而减少个体的计算数量,降低运算量,同时给出该方法的相关理论分析和证明过程。然后,针对一系列三目标优化问题,将提出方法与著名排序方法NSGAII,及近年来优秀的ENS方法进行对比实验。仿真实验结果表明,提出方法在时间复杂度和收敛速度上优于经典方法,稍差于ENS方法。在标准测试函数DTLZ1-DTLZ6的性能上,提出方法近似于ENS方法,优于NSGAII算法,从而验证了提出方法的有效性和正确性。     

Survey of GPU Based Sorting Algorithms

Parallel sorting algorithms are widely studied nowadays. After the introduction of parallel processors such as graphics processing unit (GPU) and easy to use parallel programming languages such as CUDA and OpenCL, literature on parallel sorting algorithms has become vast and richer with new ideas and techniques applied to solve the famous problem of sorting. This paper presents a survey of GPU based sorting algorithms. Four sorting algorithms have been selected for this survey: Radix sort, Merge sort, Sample sort and Quick sort. Methods used in those algorithms are described in brief. The performance of these algorithms as claimed by their authors is also presented. A comparative analysis based on the literature is depicted.     

一种三路划分快速排序的改进算法

快速排序是一种经典的排序算法,它的平均性能非常突出。针对快速排序在某些特殊情况下(如数据已有序或重复数据较多时)效率较低的问题进行了研究,对三路快速排序进行改进,使快速排序在特殊情况下也能保持较好的效率。通过大量的数据测试发现,该算法在最好情况下其性能在几个数量级上优于普通快速排序,在最坏情况下,其性能较普通快速排序无明显差距。改进后的三路快速排序是一种通用高效的排序算法,因此在某些情况下选用、该算法会获得更好的效率。     

Efficient sorting design on a novel embedded parallel computing architecture with unique memory access

Embedded Parallel computing architecture with Unique Memory Access (ePUMA) is a domain-specific embedded heterogeneous 9-core chip multiprocessor, which has a unique design with low power and high silicon efficiency for high-throughput DSP in emerging telecommunication and multimedia applications. Sorting is one of the most widely studied algorithms, more embedded applications also need efficient sorting. This paper proposes an efficient bitonic sorting algorithm eSORT for the novel ePUMA DSP. eSORT algorithm consists of two parts: an in-core sorting algorithm and an intra-core sorting algorithm. Both algorithms are adapted to the novel architecture and take advantage of the ePUMA platform. This paper implemented and evaluated the eSORT for variable datasets on ePUMA multi-core DSP and compared its performance with the Cell BE processors with the same SIMD parallelization structure. Results show that bitonic sort on ePUMA multi-core DSP has much better performance and scalability. Compared with optimized bitonic sort on Cell BE, the in-core sort is 11 times faster and intra-core sort is 15 times faster in average.     

程序设计中常用的排序算法

针对程序设计中常出现的排序问题,介绍了六种常用的排序算法:插入排序、希尔排序、堆排序、归并排序、冒泡排序、快速排序,以及每种排序所需的时间复杂度,当对大量的数据排序时,以选择适应的算法,提高程序的执行速度。     

程序设计中常用的排序算法

针对程序设计中常出现的排序问题，介绍了六种常用的排序算法：插入排序、希尔排序、堆排序、归并排序、冒泡排序、快速排序，以及每种排序所需的时间复杂度，当对大量的数据排序时，以选择适应的算法，提高程序的执行速度。     

“内部排序算法”可视化教学软件的设计与实现

介绍了利用C#开发"内部排序算法"可视化教学软件的方法,实现了快速排序、冒泡排序、堆排序、直接插入排序、折半插入排序等基本算法的动态演示。软件动态演示排序算法的抽象性、动态性,使学生直观、清晰地掌握学习排序算法,从而达到辅助教学,提高教学效果的目的。     

Generalized methods for algorithm development on optical systems

A number of recent studies have revealed that the Optical Transpose Interconnection Systems (or OTIS) are promising candidates for future high-performance parallel computers. In this paper, we present and evaluate two general methods for algorithm development on the OTIS. The proposed methods are general in the sense that no specific factor network or problem domain is assumed. The proposed methods allow efficient mapping of a wide class of algorithms into the OTIS. These methods are based on grids and pipelines as popular structures that support a vast body of parallel applications including linear algebra, divide-and-conquer type of algorithms, sorting, and FFT computation. Timing models for measuring the performance of the proposed methods are also provided. Through these models, the performance of various algorithms on the OTIS are evaluated and compared with their counterparts on conventional electronic interconnection systems. This study confirms the viability of the OTIS as an attractive alternative for large-scale parallel architectures. Finally, we show how the proposed methods can be used to design parallel algorithms for linear algebra on the OTIS.