共查询到20条相似文献,搜索用时 62 毫秒
1.
CBTC(Communication Based Train Control,基于通信的列车控制)系统的联锁软件为SIL4级的高安全、高可靠软件,目前广泛使用的软件测试和仿真验证的结果严重依赖选取的测试向量,要保证高覆盖率的测试十分困难。EN50128中强烈推荐SIL4等级的软件使用形式化方法完成软件需求规格说明书和软件设计,因此,采用形式化的方法设计软件,是构造高可靠、高安全软件的一个重要途径。本文总结了现有的CBTC系统中联锁子系统集成方式及优缺点,并使用事件确定有限自动机ETDFA(Event deterministic finite automata)模型对适用性更优的升级型集成方式的联锁软件的联锁逻辑完成形式化定义,保证联锁逻辑的正确性,减少软件的不确定性描述。以办理进路为例生成联锁对象的ETDFA模型,验证该方法的有效性和可行性。该方法不仅为CBTC联锁软件的设计与开发提供新思路,而且有助于安全苛求软件的形式化验证与分析,提高联锁软件的安全性和正确性。 相似文献
2.
随着机器人应用在越来越多的领域,人们对其安全性的要求越来越高,作为机器人的核心,控制系统设计的可靠性对整个系统的安全至关重要;针对一种模块化设计的机器人控制系统架构,利用xMAS(eXecutable MicroArchitecture Specification,可执行微架构描述)模型在定理证明器ACL2中对其功能正确性进行验证,首先对Xmas在ACL2中的形式化理论做了阐述,然后对该机器人控制系统中的加速度传感器数据采集模块建立xMAS模型,提取关键属性并进行验证;将xMAS模型和定理证明器ACL2相结合,可以很好地解决机器人控制系统的验证问题,为机器人控制系统的形式化验证提供一个有效的方法参考。 相似文献
3.
由于人为误操作和数据库系统异步因素,电力系统监控数据存在错误风险,需要对监控数据进行多点校核来保障其一致性和正确性,可靠的监控数据保证电力系统的安全运转;然而多点校核业务流复杂且对数据精度要求高,目前的人工校核方法不仅成本高,且精度和效率低,不能保证整个监控数据的实时校核工作;为自动化监控数据多点校核过程,需要对整个业务流建模,针对该问题,提出一种基于Petri网的监控数据多点校核动态建模方法;首先将监控系统的校核业务背景形式化Petri网中的具有不同约束的节点;然后使用工作流Petri方法对校核的业务流程进行形式化定义、并将该业务流程用Petri网建模成为网状模型;最后,针对该模型提出一种化简技术对其进行化简,并证实该化简方法的有效性和该模型能拟合监控数据多点校核的整个流程。 相似文献
4.
随着机器人应用在越来越多的领域,人们对其安全性的要求越来越高,作为机器人的核心,控制系统设计的可靠性对整个系统的安全至关重要。针对一种模块化设计的机器人控制系统架构,利用xMAS(eXecutable MicroArchitecture Specification,可执行微架构描述)模型在定理证明器ACL2中对其功能正确性进行验证,由于xMAS模型在ACL2中的形式化工作并不完全,首先补充和改进了xMAS在ACL2中的形式化工作,然后对该机器人控制系统中的串口模块建立xMAS模型,提取关键属性并进行验证。本文将xMAS模型和定理证明器ACL2相结合,可以很好地解决机器人控制系统的验证问题,为机器人控制系统的形式化验证提供一个有效的方法参考。 相似文献
5.
由于人为误操作和数据库系统异步因素,电力系统监控数据存在错误风险,需要对监控数据进行多点校核来保障其一致性和正确性,可靠的监控数据保证电力系统的安全运转。然而多点校核业务流复杂且对数据精度要求高,目前的人工校核方法不仅成本高,且精度和效率低,不能保证整个监控数据的实时校核工作。为自动化监控数据多点校核过程,需要对整个业务流建模,针对该问题,提出一种基于Petri网的监控数据多点校核动态建模方法。首先将监控系统的校核业务背景形式化Petri网中的具有不同约束的节点;然后使用工作流Petri方法对校核的业务流程进行形式化定义、并将该业务流程用Petri网建模成为网状模型;最后,针对该模型提出一种化简技术对其进行化简,并证实该化简方法的有效性和该模型能拟合监控数据多点校核的整个流程。 相似文献
6.
针对舰船嵌入式软件手动测试的弊端,首先从业务逻辑、接口类型等方面总结了舰船嵌入式软件的特点,从测试用例的建模、形式化转换以及用例的解析3个方面提出了测试用例自动驱动方案,在此基础上,根据舰船嵌入式软件的业务逻辑,研究了测试用例建模方法,包括测试用例数据模型、行为模型和测试用例模型特性,给出了测试用例自动驱动方法,并且以上述方法为基础对测试用例自动驱动平台进行了设计,给出了平台硬件组成和软件设计方案;最后,利用测试用例驱动平台对某软件进行了测试应用验证,验证结果表明利用测试用例驱动平台可以显著提高测试效率。 相似文献
7.
8.
强流重离子加速器装置(HIAF)的增强器(BRing)二极铁电源样机采用多模块串并联的全储能快循环脉冲电源实现方案,电源功率达到MW级。由于电源规模庞大和功率巨大,为了在运行中迅速保护电源设备,设计并实现了一套双冗余的基于可编程逻辑控制器(PLC)、模块故障联锁板和现场可编程门阵列(FPGA)的模块故障联锁保护系统,利用硬件和软件同时对电源功率单元模块实施故障检测、故障传递和故障保护。设计完成后分别从电源联锁环路的响应时间、核心控制板故障引发电源环路联锁的总时间和设备故障响应等三个方面进行测试,测试结果表明,在电源发生故障时,模块故障联锁保护系统满足电源样机对实时性和可靠性的要求,达到设计目标。 相似文献
9.
新一代运载火箭采用低温动力技术,测量系统获取飞行过程遥测参数的同时,需要完成火箭发射前低温推进剂加注期间压力、温度等关键参数的可靠获取。相比传统火箭,对测量系统在供配电和地面测控的可靠性设计、连续工作时间、测试性、扩展性和箭地接口设计提出了较高要求,对此文中提出了一种基于1553B总线的供电测控系统,介绍了系统的硬件和软件组成、功能和测控信息流向,分析了系统设计的4项关键技术:单机设备智能化设计、箭地接口简化设计、总线通信协议和高可靠PXI冗余备份设计。设计的新型供电测控系统在新一代运载火箭各项大型地面试验中成功实现了工程应用,系统方案设计的正确性得到了充分验证,系统方案在其他项目中得到了推广。 相似文献
10.
11.
兰州重离子加速器(简称HIRFL),是我国规模最大、加速离子种类最多、能量最高的重离子研究装置,可提供单核子能量达GeV量级的重离子束。HIRFL运行时,束流会在加速器隧道内产生辐射,需要建立一套人身安全联锁系统来保障人员的辐射安全。HIRFL人身安全联锁系统遵循分区联锁、硬件最可靠、失效保护、冗余及独立性、自锁等设计原则,选用了可靠性高的冗余PLC作为核心控制器,并使用了安全性高的联锁部件。本工作的完成保障了HIRFL工作人员的辐射安全,也为同类型加速器装置的人身安全联锁系统设计提供了参考。 相似文献
12.
正电子发射断层成像PET (Positron Emission Tomography)是一套庞大、复杂而又极其精密的大型医疗设备,由成千上万个探测单元及相应的信号采集通道组成,其复杂的采集逻辑直接导致系统前期研发迭代次数多、硬件调试困难,且时间与资金成本投入高。本文通过研究PET系统整体结构及前端电子采集模块的功能,设计出基于Gate仿真软件(Geant4 application for tomographic emission)和MATLAB (matrixlaboratory,Mathworks Inc.)数据处理包的PET电子学仿真架构,利用数字化单事件重建DiSER (digitalsingle-event-reconstruction)模型将Gate仿真得到的湮灭事件的能量、时间信息进行综合,转换为光子脉冲信号并由模数转换器ADC (analog-to-digital converter)进行量化,量化数据输入到现场可编程门阵列FPGA (field programmable gate array)和MATLAB协仿真模块中,验证FPGA硬件采集算法的可行性。待各模块的湮灭事件采集完毕,将多模块数据进一步综合输入到FPGA符合处理模块中,完成PET系统符合单元的功能验证。最后,将设计的算法在基于飞行时间技术的TOF (time-of flight)-PET样机上进行了测试,验证了设计的有效性和正确性。该系统仿真平台可应用于PET系统整个研发周期,其搭建思路也可灵活、有效地拓展到其他领域的系统建模与验证之中。 相似文献
13.
阐述了采用PCI接口芯片和FPGA技术研制阻性电子负载卡的方法,重点分析了基于FPGA芯片控制逻辑的实现方法,总结了使用接口芯片开发PCI总线板卡的关键要点和开发驱动软件的步骤;通过在航空测试系统中的实际应用,验证了该PCI阻性电子负载卡的设计能够达到航空修理领域对电阻模拟的实时响应性、准确性的需求。 相似文献
14.
15.
16.
17.
雷达系统内部含有多种带有光纤接口的数字电路模块,对于这类电路板的测试问题,文中提出了一种构建自动测试系统的通用方法。基于CPCI总线的多功能光纤测试模块作为该测试系统的核心测试部件,对外提供10个可收发的光纤接口,光纤接口数据传输速率可在一定范围内设定,以匹配被测模块的光口速率要求,协议数据包可按用户自定义方式发送和录取,解决了被测模块的多光口测试,光口数据传输速率不统一,数据包格式各不相同的等问题。整个测试过程可由软件控制自动完成。该测试系统能够实现对标准总线和非标准总线的光纤接口雷达数字模块的自动测试,经过实际测试验证表明,该系统运行稳定可靠,提高了武器装备的综合保障能力。 相似文献
18.
中国散裂中子源(CSNS)加速器真空控制系统负责真空数据采集、设备监控和闸板阀控制与联锁,是设备运行和故障诊断以及超高真空保持的重要保障。本文介绍了加速器真空需求,基于实验物理及工业控制系统EPICS软件框架的真空控制系统设计与实现,使用横河可编程逻辑控制器PLC控制与联锁设备,摩莎MOXA工控机监测真空状态,EPICS PV数据直接进入声音报警系统和历史数据库系统,为工作人员及时发现和处理问题、进行后续数据分析和机器研究等提供了便捷途径和可靠保障。目前,该系统已完成现场安装和调试,并已正式投入运行。运行结果表明,该系统具有稳定性好、可靠性高、人机交互友好的特点,很好地满足了加速器真空控制系统运行的需要。 相似文献
19.