识别时间自动机中可加速环的方法

为了实现精确加速从而解决由于不同时间度量而造成的模型检测时出现的片段问题,提出了一种识别时间自动机中可加速环的方法.针对时间自动机规模较大的问题,在识别可加速环的方法中引入拓扑排序的思想,通过简化时间自动机的规模,提高了识别时间自动机中可加速环的效率.实例验证和复杂度分析表明该方法是可行的.     

实时并发系统的PTSL模型检测

随着实时并发系统的软件规模越来越大、复杂性日趋增加,如何保证并发实时系统正确性和可靠性成为日益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质,它不仅包括对系统模型的遍历以及基于图形的分析方法,而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型（CGS）的扩展,在此基础上添加了概率与时间性质,提出了概率时间并发博弈结构（PTCGS）。同时本文还提出了新的逻辑语言-概率时间策略逻辑（PTSL）,它显式地把策略作为一阶逻辑中的对象,从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求,从而提高系统的可靠性。最后,本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。     

基于时间自动机的Web服务模型检测

传统的基于有限状态机的组合Web服务模型检测方法不能保证带有时间约束的组合Web服务的正确性.把组合Web服务看成多智能体系统,将带有时间约束的Web服务智能体建模为时间自动机,通过并发组合构成时间自动机网络,从而用时间自动机验证工具UPPAAL对组合Web服务的运行过程进行模拟,并验证其活性、安全性和死锁等性质.采用该方法对雇员出差安排组合Web服务进行建模和验证,结果表明,该组合Web服务存在死锁问题.最后通过分析死锁产生的路径,完善该组合Web服务的通信协议,从而消除了死锁.     

基于模型剪枝和半精度加速改进YOLOv3-tiny算法的实时司机违章行为检测

为解决在嵌入式设备上实时、高精度检测司机安全驾驶监督的问题,本文基于目标检测中经典的深度学习神经网络YOLOv3-tiny,运用通道剪枝技术成功在目标检测任务中实现了模型压缩,在精度不变的情况下减少了改进后神经网络的计算总量和参数总数.并基于NVIDIA的推理框架TensorRT进行了模型层级融合和半精度加速,部署加速后的模型.实验结果表明,加速模型的推理速度约为原模型的2倍,参数体积缩小一半,精度无损失,实现了高精度下实时检测的目的.     

虚拟装配中基于精确模型的碰撞检测算法

针对目前虚拟装配中由多边形模型引起的碰撞检测准确性低的问题,提出一种考虑公差信息的精确碰撞检测算法.首先进行分层的多边形碰撞检测,获得发生碰撞的多边形;然后基于层次图像数据将发生碰撞的多边形映射到零件相应的几何上;再依据几何的公差信息计算碰撞阈值;最后根据碰撞阈值进行精确碰撞判定.实例验证结果表明,文中算法在保证虚拟装配系统实时性的同时,提高了碰撞检测的准确性.     

基于加权移动窗口入侵检测系统模型

本文首先简要介绍了移动窗口的工作原理,加权的移动窗口概念及原理。该方法能够识别并适应概念飘移,根据数据流的概念漂移的状况自动调整训练窗口并对检测模式进行及时的更新,从而可以作为一种入侵检测的方法。在该理论的基础之上设计了基于加权移动窗口入侵检测系统模型,实现了该框架的一个系统原型。     

基于虚拟窗口的图像加速显示和重画技术

叙述了图像系统开发中提高图像显示和重画速度的重要性,详细讨论了基于虚拟窗口的图像加速原理及实现方法.     

数据流层次窗口模型及聚集查询算法

本文提出了一种多层次时间窗口模型,支持在不同时段对数据流进行不同粒度的建模,并给出了多粒度聚集树结构及其数据流聚集查询算法,从而有效地解决了在有限时空条件下的数据流聚集查询问题。     

基于加权移动窗口的入侵检测算法研究

为克服目前入侵检测技术检测反应速度慢、误检率和漏检率较高等问题,研究了加权移动窗口这种数据挖掘方法。首先对现有的移动窗口算法MFI-TransSW和Moment进行了认知与分解,指出现有算法的缺陷,提出了加权移动窗口的详细算法,自动调整训练窗口,并对检测模式进行及时的更新;在此基础上建立了基于加权移动窗口的入侵检测系统模型。最后实例检测和结果分析表明,在不同窗口大小、不同最小支持度、数据集增大时该算法执行时间均优于其他算法。     

基于模型分解的多机带时间窗口任务规划算法

针对多机带时间窗口任务规划问题,提出了基于模型分解的规划求解算法。通过引入基于逻辑的Benders分解方法,将经典Benders分解算法应用扩展至带离散时间窗口的混合线性整数规划模型,实现模型分解。采用工艺级商业软件MOSEK与GECODE分别求解主、子问题,同时给出Benders剪枝函数生成方法,以迭代方式收敛解空间获得可行解。实现算法并设计测试案例,实验结果验证了算法的有效性。     

一种层次式时间自动机模型检测方法

层次式时间自动机在软件系统建模过程中有着重要的应用.由于层次嵌套带来额外的复杂度,难以对之进行直接的形式化验证工作.提出一种平展算法,将层次式时间自动机转化为一组并行的顺序时间自动机,应用广播通道同步该自动机集合执行.在此基础之上实现一个原型系统可以将层次式时间自动机模型自动转化为模型检测工具UPPAAL的输入,从而可以对之进行验证.结合实时UML状态机图实例,证明了该方法的有效性.     

带时间约束的LTL性质的模型检测的实现

针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束,在对性质自动机和模型自动机的复合进行空性检测时,通过使用不同方法对如何获取性质自动机迁移边上的时间约束进行了研究,实现了对带时间约束的线性时序逻辑性质的检测,扩展了工具CATV的检测范围,方便了用户的使用。     

基于轴对称窗口文字图像检测快速算法研究

研究了图像定位的问题,由于存在污渍干扰等影响图像定位,针对以往单一特征进行图像文字定位及识别的系统中容易受到各种环境因素干扰的缺陷,提出了一种利用轴对称窗口进行边缘检测的图像文字检测算法。首先将利用轴对称滑动窗口提取水平和竖直方向上的边缘特征,利用连通域确定初始的图像文字位置;通过对可能的图像文字区域进行颜色色调验证,区域内垂直方向直方图投影,从而确定最终的图像文字位置。由于利用多种特征综合检测图像文字进行仿真。仿真结果表明改进方法能准确检测出复杂场景下图像文字所在区域。     

紧凑等离子体环整体加速过程的数值计算

紧凑等离子体环（CT）应用广泛,可以作为聚变驱动源和脉冲X射线源等,对CT加速过程的研究是其应用方面研究的基础．描述了CT加速的基本原理,基于整体加速模型导出数值模拟方程组,采用四阶龙格-库塔法数值求解此方程组．根据Phillips实验室MARADUER的参数和SHIVA—STAR电容器组参数,对CT在同轴加速器内的加速过程进行了数值模拟,定量地分析了影响加速效率的各种因素．计算结果表明：CT的质量越大、加速器越长,加速效率越高,但加速效率存在饱和趋势;电感和电阻越小,加速效率越高;对于一定的电容器初始储能,电容值较小时加速效率越高．     

基于窗口法的改进锋电位检测算法

针对窗口检测法在窗口间存在重复检测和检测时间代价大等问题,提出一种新的锋电位峰值检测算法。该方法以改进的窗口检测法为基础,结合阈值法对锋电位进行检测。所提出的方法在来源于英国莱斯特大学的仿真数据上进行了验证,实验表明,该方法在不影响运行时间的同时,在误报率和漏报率方面相对于阈值检测法和窗口检测法有明显降低。     

卫星时间窗口计算的动态步长快速算法

针对卫星轨道连续跟踪采样的时间窗口传统计算方法计算量大、效率低的问题,提出了一种新的快速算法。为减少参与计算的采样点数量,算法通过预测参与计算对象之间距离动态调整采样步长;为使算法适于解决各类时间窗口计算问题,提出广义可视概念进行时间窗口判定。分别研究了卫星与地面点目标可见时间窗口、星间可见时间窗口、卫星对地面目标覆盖时间窗口、地面大范围区域卫星过境时间窗口的广义可视判断方法和预测距离计算模型。实验结果表明,算法与传统算法精度完全一致,效率提升约99.7%。     

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

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

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

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

一种改进型级联神经网络检测算法及加速处理

为提高MTCNN网络检测准确度,且针对检测密集样本容易漏检的问题,通过改进网络隐藏层结构提高网络学习能力,通过Soft-NMS惩罚置信度方式筛选检测框,提高了网络检测准确度,针对密集样本仍保持高精度;且为提高改进后网络推理速度和克服网络依赖PC端资源问题,基于HLS实现了网络加速推理。实验结果表明,改进后各子网络检测准确度由93.73%、95.30%、95.89%提高至94.78%、96.30%、97.55%,密集样本测试集测试准确度为97.21%;使用硬件加速对比2.9GhzCPU推理速度快3.3倍,硬件资源最大占用91%,较好利用硬件资源实现了加速处理。     

多处理器实时系统可调度性分析的UPPAAL模型

随着多处理器实时系统在安全性攸关系统中的广泛应用,保证这类系统的正确性成为一项重要的工作.可调度性是实时系统正确性的一项关键性质.它表示系统必须满足的一些时间要求.传统的可调度性分析方法结论保守或者不完备,为了避免这些方法的缺陷,提出使用模型检测的方法来实现可调度性分析.提出了一个用于多处理器实时系统可调度性分析的模板,将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模,并使用UPPAAL验证可调度的性质是否总被满足.符号化模型检测方法被用于推断可调度性,但是由于秒表触发的近似机制,符号化模型检测方法不能用于证明系统不可调度.作为补充,统计模型检测方法被用于估算系统不可调度的概率,并在系统不可调度时生成反例.此外,在系统可调度时,通过统计模型检测方法获取一些性能相关的信息.