一个命题投影时序逻辑符号模型检测器

现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection temporal logic,简称PPTL)符号模型检测工具——PLSMC(PPTL symbolic model checker)的设计与实现过程.该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模型检测算法.PLSMC的规范语言PPTL具有完全正则表达能力,这使得定性性质和定量性质均可被验证.此外,PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题.最后,利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证.实验结果表明,PPTL符号模型检测工具扩充了NuSMV系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证.

基于概率模型检测器的核电厂分布式控制系统动态可靠性分析

分布式控制系统(DCS)是核电厂的神经中枢,对其进行可靠性分析,识别薄弱环节,开展有针对性的设计优化和运维改进,提高电厂安全水平。DCS部件存在备用自投、在线修复等动态行为,传统故障树不能充分描述上述动态行为。针对上述问题,采用马尔科夫模型建立完整的DCS子系统可靠性模型,包括操作终端、PU处理单元、交换机,以及处理器、电源等各类模件,采用概率模型检测器PRISM对马尔科夫模型进行定量计算,得到系统的不可用率,并对系统各失效状态维修率进行了敏感性分析,结果表明,操作与监视系统(OM690)、电厂总线和采集卡失效对系统不可用率的贡献高达95%,因此,通过增加OM690系统、总线设备、采集卡的备件数量和维护人力,可有效提高上述设备的可靠性。

多值可能性模型检测器的设计与实现

随着现代计算机软件和硬件的复杂性变大,模型检测作为一种形式化自动验证技术,与传统的检测技术相比有着一系列的优势,比如可以在系统实现之前对系统进行验证,可以提前发现问题,节约大量成本。传统的模型检测器大多是基于经典的模型检测技术实现的,而现实生活中存在大量的不确定信息,使用传统的模型检测无法解决这些问题。而多值模型检测理论的出现,结合多值计算树逻辑,构建多值可能性Kripke结构模型,可以很好地解决这些问题。为了实现模型检测自动化特性的最大优势,基于多值可能性定量模型检测的理论,设计了多值Kripke结构在计算机中的存储结构、计算模块等,实现了一个基于多值可能性测度的多值计算树逻辑的模型检测器MvChecker,使得用户可以自动验证系统性质。

疫苗独立机制的免疫入侵检测器模型研究

该模型将疫苗模块以独立的形式引入到免疫检测器模型中,通过信号控制疫苗接种模块与疫苗抽取模块的运作,对已有抗体的检测器中的记忆检测器集合动态提取成熟疫苗,注入需要接种检测器的成熟检测器集合中,使得不同检测器在运作过程中以疫苗作为媒介相互通信,随时共享抗体(检测器),这样增加了检测器的灵活性。通过MATLBE仿真实验,对加入疫苗独立机制的检测器进行网络数据检测。结果显示,基于疫苗独立机制的免疫入侵检测器模型响应更快,检测率TP更高,误检率FP较低,证明该模型有更好的综合检测性能。

基于残差单发多框检测器模型的交通标志检测与识别

针对现有目标检测方法仅适用于大尺寸、少量特定种类交通标志的检测,且对复杂交通场景图像检测效果不佳的问题,以抗退化性能较强的ResNet101为基础网络,增加若干卷积层构建残差单发多框检测器(SSD)模型,对高分辨率的交通图像进行多尺度分块检测。为了加快检测速度,采取由粗到精的策略,省略对纯背景图像块的预测.利用中等尺度图像块的初检结果缩小目标范围;对目标范围内的其他图像块进行检测;将所有图像块结果映射回原图像,并结合非极大值抑制实现精准识别。实验结果表明,该模型在公开的交通标志数据集Tsinghua-Tencent 100K上取得了94%的总体准确率和95%的总体召回率,对多分辨率图像中不同大小和形态的交通标志都具有良好的检测能力,鲁棒性较强。

基于概率模型检测的SysML活动图验证方法

针对系统建模语言(systems modeling language,SysML)活动图模型无法进行精确的形式化分析与验证的问题,在研究现有模型检测的基础上,提出使用概率模型检测器(PRISM)对SysML活动图模型进行检测的分析验证框架,并提出一种把SysML活动图转化为相应的PRISM可执行模型的转化规则。利用该转化规则可以把SysML活动图模型转化为概率模型检测器支持的格式,实现对模型的精确分析和定量验证。实验结果表明,该规则能够有效对SysML活动图模型进行转化,为模型检测提供支持。

基于BDMP模型的核电厂稳压器水位控制系统可靠性分析

稳压器水位控制系统(PLCS)承担一回路冷却剂装量调节功能,是核电厂分布式控制系统(DCS)的关键子系统之一。本文采用布尔逻辑驱动的马尔科夫(BDMP)模型构建PLCS动态可靠性模型,并提出了一种将BDMP转换为马尔科夫模型的方法,采用概率模型检测器PRISM对转换所得马尔科夫模型进行定量计算,得到了PLCS的不可用率及不同部件对不可用率的贡献值,然后采用KB3和YAMS进行建模与定量计算,将结果与PRISM结果进行比较,验证了本文方法的有效性。本文方法为核电厂稳压器水位控制系统设备维修的侧重提供了方向和参考。

结合注意力机制和特征融合的小目标检测方法

图像中的小目标物体所占像素较少,存在特征难以提取,容易出现漏检的问题,在单次多框检测器(single shot multi-box detector, SSD)模型基础上,提出了一种结合注意力机制和特征融合的小目标检测方法。首先,采用ResNet50网络作为特征提取骨干网络,解决原网络梯度相关性衰减导致特征提取能力不足的问题;然后,在低层特征提取层中加入注意力机制模块,通过抑制无关信息,提高网络对低层特征的学习能力;最后,将低层特征与高层语义信息进行级联融合,充分利用不同特征图之间的关联信息。实验结果表明:改进模型对小目标物体检测平均精度均值达到51.1%,比改进前提高了9.3%,有效提高了小目标物体的检测精度。

多尺度语义信息融合的目标检测

针对当前目标检测算法对小目标及密集目标检测效果差的问题,该文在融合多种特征和增强浅层特征表征能力的基础上提出了浅层特征增强网络(SEFN),首先将特征提取网络VGG16中Conv4_3层和Conv5_3层提取的特征进行融合形成基础融合特征;然后将基础融合特征输入到小型的多尺度语义信息融合模块中,得到具有丰富上下文信息和空间细节信息的语义特征,同时把语义特征和基础融合特征经过特征重利用模块获得浅层增强特征;最后基于浅层增强特征进行一系列卷积获取多个不同尺度的特征,并输入各检测分支进行检测,利用非极大值抑制算法实现最终的检测结果。在PASCAL VOC2007和MS COCO2014数据集上进行测试,模型的平均精度均值分别为81.2%和33.7%,相对于经典的单极多盒检测器(SSD)算法,分别提高了2.7%和4.9%;此外,该文方法在检测小目标和密集目标场景上,检测精度和召回率都有显著提升。实验结果表明该文算法采用特征金字塔结构增强了浅层特征的语义信息,并利用特征重利用模块有效保留了浅层的细节信息用于检测,增强了模型对小目标和密集目标的检测效果。

多尺度卷积特征融合的SSD目标检测算法

提出了一种改进的多尺度卷积特征目标检测方法,用以提高SSD(single shot multibox detector)模型对中目标和小目标的检测精确度。该方法先对SSD模型低层特征层采用区域放大提取的方法以提高对小目标的检测能力,再对高层特征层进行特征提取以改善中目标的检测效果。最后,利用SSD模型中原有的多尺度卷积检测方法,将改进的多层特征检测结果进行融合,并通过参数再训练以获得最终改进的SSD模型。实验结果表明,该方法在MS COCO数据集上对中目标和小目标的测试精确度分别为75.1%和40.5%,相比于原有SSD模型分别提升16.3%和23.1%。

可见光图像目标检测技术综述

可见光图像目标检测是计算机视觉中的研究热点和难点。对目标检测技术的三个核心问题——目标表述、目标检测模型训练和目标检测定位的研究现状进行了综述，并对目标检测技术的下一步研究方向进行了探讨。

基于BDMP的反应堆冷却剂平均温度控制系统动态可靠性分析

反应堆冷却剂平均温度控制系统(RCATCS)是核电厂安全重要仪控系统之一,对保证核电厂的正常运行起着重要作用。采用布尔逻辑驱动的马尔科夫过程(Boolean logic Driven Markov Process,BDMP)构建RCATCS动态可靠性模型,并采用概率模型检测器PRISM对其进行定量分析,得到了RCATCS的不可用率及系统各部分对不可用率的贡献值。最后,通过对比KB3和YAMS的BDMP定量分析结果,验证了该方法的有效性。结果表明,定量分析的计算效率明显提高,为核电站RCATCS设备的维修侧重提供了参考和方向。

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

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

国产重型燃气轮机控制系统可靠性分析

提升可靠性是国产化重型燃气轮机控制系统研发需要解决的核心问题。硬件冗余是控制系统可靠性的重要保障,可在功能上实现容错,其成本与故障修复相比更低,已在工业应用中占据主导地位。由于我国重型燃气轮机控制系统的研制还处于攻关阶段,对其可靠性的研究几乎处于空白状态。分析了国产重型燃气轮机NuCON控制系统的冗余策略,采用马尔可夫(Markov)模型构建该冗余策略下的可靠性模型;运用概率模型检测器PRISM对可靠性模型进行定量计算和检验,仿真表明,在一定修复时间和冗余结构下,采用最小硬件配置的NuCON控制系统的不可用率为1.616×10-4,满足系统可靠性设计要求。同时对比分析了不同修复时间、不同系统结构和不同系统规模对系统不可用率的量化影响结果。

基于机器视觉的割草系统青草识别研究

为使割草机系统实现青草识别,规划割草机运动路径并自动进行割草工作,采用单步多框检测器(SSD)目标检测算法和卷积神经网络框架(Caffe)在工作机上训练青草识别模型.通过树莓派(RPi)拍摄割草场地照片并传送到工作机,工作机计算青草在图片中的坐标值并返回至树莓派,树莓派再根据青草的坐标值自动计算车桥转动角度和后轮电动机运行时间及方向,调动割草机机械部分进行割草作业.实验结果表明,较之于传统的人工机械割草机或围栏式割草机,训练的青草识别模型能正常识别青草,割草机能较好地自动规划割草路径,具有一定除草效果.研究结果实现了机器视觉和传统机械的结合,为今后智能机械的研究提供一定思路.

基于UML-NuSMV的并发系统建模与验证

为解决直接建立系统NuSMV(符号模型检测器)模型的困难,提出一种从UML(统一建模语言)模型转换到NuSMV模型的方法,实现了UML与NuSMV结合的形式化验证.首先,使用UML中的视图对系统进行描述,建立系统的UML模型;然后,设计转换规则并给出转换算法,实现从UML模型到NuSMV模型的自动转换;最后,使用计算树逻辑对系统的属性进行描述,并通过NuSMV完成对系统的形式化验证.以一个双按键并发电梯系统为例,说明了基于UML-NuSMV的并发系统建模与验证过程.