多基准站GPS定位靶场测试方法研究

CBTC(Communication Based Train Control,基于通信的列车控制)系统的联锁软件为SIL4级的高安全、高可靠软件,目前广泛使用的软件测试和仿真验证的结果严重依赖选取的测试向量,要保证高覆盖率的测试十分困难。EN50128中强烈推荐SIL4等级的软件使用形式化方法完成软件需求规格说明书和软件设计,因此,采用形式化的方法设计软件,是构造高可靠、高安全软件的一个重要途径。本文总结了现有的CBTC系统中联锁子系统集成方式及优缺点,并使用事件确定有限自动机ETDFA(Event deterministic finite automata)模型对适用性更优的升级型集成方式的联锁软件的联锁逻辑完成形式化定义,保证联锁逻辑的正确性,减少软件的不确定性描述。以办理进路为例生成联锁对象的ETDFA模型,验证该方法的有效性和可行性。该方法不仅为CBTC联锁软件的设计与开发提供新思路,而且有助于安全苛求软件的形式化验证与分析,提高联锁软件的安全性和正确性。     

Extending Petri net to reduce control strategies of railway interlocking system

In our previous articles we gave step by step refinement process towards the development of safety properties of moving block interlocking system (MBRIS). The refinement process started from abstraction to fuzzy based safety properties using Z and then fuzzy multi agent specification language. However, one dimensional control of train passing through a switch and level crossing were not discussed. This paper reduces the existing two dimensional controls along the switch and level crossing to one dimensional for shifting it to a train only. For example, in the existing model the train movement along components switches and level crossings depends on both the train and components control. Whereas, in one dimensional control train is the only authority to control a switch and level crossing required for its desired operation. For this reduction, concurrent and mobile agent concepts are required. Therefore, we integrate mobile agent concepts with Petri nets to develop the mobile Petri net (MPN) a new class of PNs. This supports both mobility and concurrency. Further, we prove that the collection of different MPNs in a connected network is a PN. This proof allowed us to use the properties of PN to verify the system. Finally, we use MPN to model the safety properties of MBRIS along the switch and level crossing. This provides one dimensional control to a train along a switch and level crossing which increases the safety of the railway interlocking system. Moreover, we use reachability graph (RG) to verify the switch and level crossing models.     

从铁钉表面镀铜浅谈低年级学生科研思维培养

以铁钉表面镀铜为例,从Cu~(2+)直接氧化Fe实验中发现问题:铜镀层凸凹不平、易脱落。基于该问题,引导学生进行文献查阅,对问题进行分析,然后设计相关实验方案,进行实验操作,从而解决问题:获得表面均匀的铜镀层。通过问题发现、问题分析、文献资料查阅、实验方案设计、问题解决的思路培养低年级学生科研思维。