矿井机车运输信号系统的Event-B建模与验证研究

人工编制联锁表难以保证联锁表的准确性,而且单纯依靠人工检查联锁表中每个表项的正确性也是一项非常繁琐的工作。文章针对目前存在的问题,利用形式化Event-B方法对机车运输信号平面布置图、进路联锁表和机车车辆运输信号设计规范进行建模,模型生成的证明义务通过与否验证了进路联锁表建立过程是否符合平面布置图和设计规范的要求,利用该种思路解决了人工检查联锁表存在的效率低和不确定性等问题。     

分层CPN在矿井馈电系统建模中的应用

矿井馈电系统是一种典型的离散事件动态系统。为了有效地对矿井馈电系统仿真,利用分层建模的思想来对矿井馈电系统的建模。对上层系统进行建模时引入复杂变迁,并在此基础上分解复杂变迁,最后利用所得的分层CPN（Hierarchical Colored Petri Net,HCPN）模型作为仿真软件的媒介,验证系统设计的合理性和安全性。通过利用CPN对矿井馈电系统建模,为最终开发出该系统的软件仿真平台奠定了良好的基础。     

离散事件控制系统规则化描述方法的研究

离散事件控制系统(DECS)是离散事件系统(DES)在控制领域的一个应用类别,具有并发性、多值性、时序性和需求易变等特点。文章分析了现有的各类逻辑层DES建模方法在DECS建模和分析方面存在的缺陷,在此基础上,运用专家系统中的规则表达方法和递阶DECS简约技术,从逻辑层角度,建立了一套规范、简洁、贴近自然语言和易于理解的DECS规则化描述方法。     

基于能量区域代理机制的移动Sink路由算法

文章提出基于能量区域代理机制的移动Sink路由算法。该算法使用剩余能量扫描算法将系统划分为若干个能量相近的区域,再在每个能量区域内构建路由信息,根据已构建的路由信息选择代理节点作为能量区域内信息存储和与Sink通信的节点,根据代理节点的分布制定Sink最小移动路径策略。仿真实验表明,在网络中使用该算法可以使网络能量得到更均衡合理充分的利用,可以很好地延长网络寿命。     

基于有色Petri网的车身网络诊断系统建模方法

文章针对车身网络诊断系统的特点,将有色Petri网和诊断系统的流程相结合,建立故障诊断的有色Petri网模型;利用有色Petri网作为工具,描述诊断仪与ECU通信之间的逻辑关系;以诊断中的Flash下载为例,建立了有色Petri网的诊断模型.仿真分析结果验证了模型的正确性和有效性,且模型有助于提高车身网络诊断系统软件的...     

基于模糊控制的规则化描述方法研究

文章针对规则化描述方法(RDM)对连续变量描述的不足,提出了一种基于模糊控制的RDM.该方法引入了模糊控制中的模糊化和解模糊化方法,实现了RDM对连续变量的描述,扩展了RDM的应用范围.仿真结果表明,基于模糊控制的RDM可应用于连续变量动态系统.     

井下无人驾驶机车运行过程控制的建模与验证

井下无人驾驶机车运行过程的控制是矿井机车无人驾驶系统(mine locomotive unmanned system,MLUS)的核心,其设计与开发具有较高的安全性要求,采用形式化方法对其需求进行建模与验证可以在开发早期验证其设计的正确性和一致性,从而较早地发现问题和解决问题。文章采用Event-B的形式化方法对井下无人驾驶机车运行过程的控制进行建模、精化和验证,采用Rodin插件ProB对机车在不同路况条件下的运行过程进行仿真,验证和仿真结果显示机车运行过程控制符合设计需求,该方法对安全性要求较高的矿井机车无人驾驶系统的设计与开发提供了新的借鉴。     

Adhoc网络中由接收者发起信道预约的节能措施

针对Adhoc网络中节点的有限能量供给问题,提出了一种基于由接收者发起信道预约的节能措施。在MACA-BI的帧中引入了数据总长、睡眠时间预测等字段,使得在不影响通信的基础上,节点尽可能处于睡眠状态,并以节点剩余能量为参数确定优先级,避免局部节点能量消耗过快,提高网络的整体寿命。