A novel refined dynamic model of high-speed maglev train-bridge coupled system for random vibration and running safety assessment

Running safety assessment and tracking irregularity parametric sensitivity analysis of high-speed maglev train-bridge system are of great concern,especially need perfect refinement models in which all properties can be well characterized based on various stochastic excitations.A three-dimensional refined spatial random vibration analysis model of high-speed maglev train-bridge coupled system is established in this paper,in which multi-source uncertainty excitation can be considered simultaneously,and the probability density evolution method(PDEM)is adopted to reveal the system-specific uncertainty dynamic characteristic.The motion equation of the maglev vehicle model is composed of multi-rigid bodies with a total 210-degrees of freedom for each vehicle,and a refined electromagnetic force-air gap model is used to account for the interaction and coupling effect between the moving train and track beam bridges,which are directly established by using finite element method.The model is proven to be applicable by comparing with Monte Carlo simulation.By applying the proposed stochastic framework to the high maglev line,the random dynamic responses of maglev vehicles running on the bridges are studied for running safety and stability assessment.Moreover,the effects of track irregularity wavelength range under different amplitude and running speeds on the coupled system are investigated.The results show that the augmentation of train speed will move backward the sensitive wavelength interval,and track irregularity amplitude influences the response remarkably in the sensitive interval.

PLC Modeling and Checking Based on Formal Method

High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of complex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduce the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the Promela language is obtained and a tool PLC-Checker for modeling and checking PLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example is found. Although the probability of this logic error occurs very small, it could result in system crash fatally.

An Augmented Framework for Formal Analysis of Safety Critical Systems

This paper presents an augmented framework for analyzing Safety Critical Systems (SCSs) formally. Due to high risk of failure, development process of SCSs is required more attention. Model driven approaches are the one of ways to develop SCSs for accomplishing critical and complex function what SCSs are supposed to do. Two model driven approaches: Unified Modeling Language (UML) and Formal Methods are combined in proposed framework which enables the analysis, designing and testing safety properties of SCSs more rigorously in order to reduce the ambiguities and enhance the correctness and completeness of SCSs. A real time case study has been discussed in order to validate the proposed framework.

Why Formal Methods Are Considered for Safety Critical Systems?

Formal methods are the mathematically techniques and tools which are used at early stages of software development lifecycle processes. The utter need of using formal methods in safety critical system leads to accuracy, consistency and correctness in proposed system. In safety critical real time application, requirements should be unambiguous and very accurate which can be achieved by using mathematical theorems. There is utter need to focus on the requirement phase which is the most critical phase of SDLC. This paper focuses on the use of Z notation for incorporating the accuracy, consistency, and eliminates ambiguity in safety critical system: Road Traffic Management System as a case study. The syntax, semantics, type checking and domain checking are further verified by using Z/EVES: a Z notation type checker tool.

Data Flow Analysis and Formal Method

Exceptions are those abnormal data flow which needs additional calculation to deal with. Exception analysis concerned abnormal flow contains a lot of research content, such as exception analysis method, program verification. This article introduces another research direction of exception analysis which based on formal method. The article analyses and summarizes those research literatures referring exception analysis and exception handling logic verification based on formal reasoning and model checking. In the article, we provide an overview of the relationship and difference between traditional ideas and formal method concerning program exception analysis. In the end of the article, we make some ideas about exception analysis based on formal semantic study of procedure calls. Exception handling is seen as a special semantic effect of procedures calls.

金融能力、正规信贷约束与农户创业行为

基于金融能力和正规信贷约束视角,利用2017年和2019年CHFS微观数据,通过构建Probit模型实证分析金融能力对农户创业行为的影响,探讨正规信贷约束在金融能力和农户创业行为关系中发挥的中介效应。结果表明:金融能力对农户创业行为具有显著正向影响,且在考虑内生性的情况下,该结论仍然成立;中介机制检验表明,金融能力能够通过缓解正规信贷约束来促进农户创业行为;异质性分析表明,中、西部地区和三线及以下城市的农户金融能力对其创业行为的影响更为显著。据此,建议建立完善的金融能力培养体系,加大对欠发达地区的政策扶持,且提高正规信贷支持力度。

基于知识图谱的建筑施工安全风险量化与分析

为了提高建筑施工安全风险管理的信息化水平,以建筑施工活动及事故风险类型为研究对象,建立施工安全知识图谱。通过知识图谱改进作业条件危险性评价法(LEC)实现安全风险的定量计算,并基于知识图谱进行风险位置识别和不安全因素分析。研究提出安全风险虚体实化理念,实现了安全风险信息在数字空间实体化表达;基于建筑信息模型(Building Information Modeling, BIM)和知识图谱技术,建立了建筑施工安全风险信息模型(Building Construction Safety Risk Information Model, BCSRIM)。该模型有效避免了传统LEC法中主观因素产生的影响,实现了建筑施工安全风险定量计算、风险位置识别、风险分析及可视化管理。利用Revit二次开发技术,在Microsoft Visual Studio中使用C#语言连接Neo4j图数据库,完成了基于知识图谱的BCSRIM的开发。试验显示,研究提出的BCSRIM对提高施工现场的管理水平具有较高的实用价值。

基于改进可拓云模型的装配式建筑施工安全风险评价方法

为保障装配式建筑施工安全,考虑到施工安全指标因素的模糊性与随机性,运用组合赋权-改进可拓云模型对施工安全风险进行评价。首先,从“三度空间”视角下,在物理、社会、信息三个层面构建了评价指标体系;其次,运用改进的层次分析法(AHP)和熵权法(EW)确定主客观权重,基于距离函数确定综合权重,根据云理论和可拓学理论提出一种云熵确定方法,对传统可拓云模型进行改进后构建评价模型;最后,将该模型运用到工程实例中,与其他模型进行对比。结果表明:该施工项目评价等级为很安全,且具有很高的可信度;验证了该模型的可靠性和可行性,为装配式建筑施工安全风险评价提供了一种更加科学、准确的评价方法。

基于MTRDL的自动飞行系统模式需求建模与验证方法

在民机自动飞行过程中,自动飞行系统模式转换是影响安全的重要因素,随着现代民机机载系统的功能与复杂度的快速增长,在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战.飞行模式转换的复杂性不仅体现在自动飞行过程中必需的多重飞行模式之间的交互关系,还体现在模式转换与外部环境之间复杂的数据与控制交联关系,这些交联关系同时隐含了飞行模式转换的安全性质,这些特征提高了形式化方法的应用难度.提出一种领域特定的建模验证框架:首先,提出面向自动飞行系统模式转换的领域需求建模语言MTRDL和基于该语言扩展于SysML上的建模方法;其次,提出基于安全需求模板的安全性质辅助规约方法;最后,通过对某机型的若干条目化需求的实例研究,证明所提方法在自动飞行系统模式转换需求验证中的有效性.

基于AADL的混合关键系统随机错误与突发错误安全性分析

许多复杂的嵌入式系统都是混合关键系统(mixed-criticality system,MCS).MCS通常需要在指定的关键性(criticality)等级状态下运行,但是它们可能会受到一些危害的影响,这些危害可能会导致随机错误和突发错误,进一步导致执行线程中止,甚至导致系统故障.目前的研究仅集中于对MCS的可调度性分析,未能进一步分析系统安全性,未能考虑线程之间的依赖关系.以随机错误和突发错误为研究对象,提出一种集成故障传播分析的基于架构的MCS安全分析方法.使用架构分析和设计语言(architecture analysis and design language,AADL)刻画构件依赖关系.为了弥补AADL的不足,创建新的AADL属性(AADL突发错误属性),并提出新的线程状态机(突发错误行为线程状态机)语义来描述带有突发错误的线程执行过程.为了将概率模型检查应用于安全分析,提出模型转换规则和组装方法,从AADL模型推导出PRISM模型.建立了两个公式,分别获得定量安全属性以验证故障发生的概率,以及定性安全属性以生成相应的正例来求出故障传播路径来进行故障传播分析.最后,以动力艇自动驾驶仪(power boat autopilot,PBA)系统为例,验证了该方法的有效性.

基于N-K-FRAM的空中交通运行安全风险耦合机制

为探究空中交通运行安全风险耦合演化特征,厘清基于N-K模型与功能共振分析方法(FRAM)相结合的空中交通运行系统耦合变异形成机制,首先,收集不安全事件文本数据,归纳事件中的风险因素并归类,得到其历史发生频率以及风险因素之间的耦合关系;其次,利用N-K模型求解运行风险因素间的耦合度值;然后,结合输出时间与精度,定量评估FRAM功能模块的可变性,分析空中交通运行安全风险耦合机制;最后,分别以区域导航(RNAV)进近不安全事件与偏离航路不安全事件为例,分析其安全风险。结果表明:基于N-K-FRAM的风险耦合机制能够合理有效地定量计算功能模块间的变异性,弱化了传统分析方法对主观意识的依赖性,分析结果更为客观科学。

基于单工架构的信息物理系统运行时安全性保障方法

运行时安全性保障方法旨在系统运行过程中确保安全性属性得到满足.基于单工(simplex)架构的运行时安全性保障方法能够在使用复杂且安全性未经验证的控制器的情况下,为系统提供安全性保证.其基本思想是将复杂且安全性未经验证的复杂控制器与经过严格形式化验证的安全控制器相结合,前者工作在无安全风险的情况下,若检测发现系统存在潜在的安全风险,则通过决策模块完成复杂控制器与安全控制器之间的切换,从而确保系统的安全性.本文重点关注基于simplex架构的信息物理系统运行时安全性保障方法,从simplex架构决策模块的设计、改进与拓展,以及simplex架构的应用3个方面展开研究,对相关工作进行了梳理和总结,指出当前面临的技术挑战,并展望未来的发展方向,认为基于simplex架构的运行时安全性保障方法将会是解决智能信息物理系统安全性保障问题的有效途径之一.

Functional safety verification and performance measurement of train-train communication link

The short-range wireless communication technology has advanced considerably and provides the feasibility of train-train(T2T)communication link in the communication-based train control system.The introduction of the T2T link would reduce the headway and improve operational efficiency.Formal methods are system design techniques that use rigorously specified mathematical models to ensure all behaviors work as expected.And it is exactly the functional safety verification needed.Therefore,to deal with the functional safety verification of the T2T link,an untimed colored petri net model is first constructed.Secondly,the verification process is performed.Conclusions can be drawn from the state space report and the computation tree logic queries.Lastly,the model is parameterized,and then data log files are obtained for further performance measurement.Results show that the proposed criteria are satisfied and there are no defects in the basic design requirements.The transmission delay has considered the reconnection,transmission errors and the interruption.The probability of the delay lower than 150 ms accounts for 98.106%,which meets the specification and the previous field test.

基于CPN的供应链合约的形式化验证

智能合约的安全性对于区块链在供应链领域的应用尤为重要。目前,大多数对智能合约的形式化验证工作集中于漏洞检测,对于如何在部署上链前生成安全的智能合约的关注仍然比较少,如何有效规范地将特定领域的属性安全地映射为智能合约代码存在难点。因此,提出在编写合约前基于CPN(Coloured Petri Net)对供应链业务逻辑进行形式化规范并构建双层仿真模型,以图形化界面描述交易状态变化,进行形式化验证和状态分析,从而在建模阶段就减少逻辑漏洞。最后,提供了一种从CPN建模语言到Solidity编写的合约的转换方法,以提高智能合约的安全性和可靠性。

基于SPIN的HMSC模型自动检验方法

自动检测与验证HMSC(high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义,为此提出一种为HMSC模型进行自动检验的方法,并将其实现。利用转换规则为HMSC模型生成Promela检测语言,借助SPIN工具对需求进行验证。该方法不仅支持模型检测,同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具,通过一个实例展示其自动建模检测分析的效果,表明了其有效性和实用性。

一种基于变量隐藏抽象的IC3硬件验证算法

随着硬件设计复杂性和规模的大幅度提升,硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术,可以自动构建反例路径,也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。为了提高验证的规模和效率,硬件验证算法设计逐渐从底层的比特级向更高的抽象级别转变。研究目标是设计一个新型有效的字级IC3算法。针对研究目标,提出了一种将变量隐藏抽象和隐式抽象结合的字级IC3算法IC3VA。该方法尝试将变量隐藏抽象和IC3算法相结合,并设计了对应的泛化和精化方案。在开源社区和硬件验证大赛收集的测试集上和基于谓词抽象的方法进行对比,实验结果显示了基于变量隐藏抽象的IC3算法的有效性。

自动飞行模式转换逻辑的形式化建模与验证

自动飞行控制系统(Automatic flight control system,AFCS)是现代飞机中重要的安全关键系统之一,飞行引导控制系统(Flight guidance control system,FGCS)是其重要的组成部分。FGCS中的飞行模式有数十种,模式转换逻辑十分复杂,在各个模式间转换时易出现模式混淆等问题,难以对其安全性和正确性进行验证。而利用计算机科学中的形式化方法,通过对安全关键系统进行形式化建模和验证,可以提高系统的正确性和安全性。本文以典型FGCS中的自动飞行模式转换逻辑作为研究对象,采用自主研制的软件工具ART(Avionics requirement tool)对其进行形式化建模与验证,并与Matlab/Simulink中的Design Verifier工具进行了验证能力和效率的对比分析。实例研究结果表明,采用形式化方法对FGCS的自动飞行模式转换逻辑进行建模、验证可行,所研制的软件平台具有更完善的验证能力和更好的验证效率。

Research on the logic monitoring method for the cloud computing based safety computer

With the development of railway construction in China,the computing demand of the train control system is increasing day by day.The application of cloud computing technology on the rail transit signal system has become a research hotspot in recent years.How to improve the safety and availability of the safety computer platform in the cloud computing environment is the key problem when applying cloud computing to the train operation control system.Since the cloud platform is in an open network environment,fac-ing many security vulnerabilities and malicious network attacks,it is necessary to monitor the operation of computer programmes through edge safety nodes.Firstly,this paper encrypts the logical monitoring method,and then proposes a secure computer de fence model based on the dynamic heterogeneous redundancy structure.Then the continuous time Markov chain(CTMC)is used to quantitatively solve the stable probability of the system,and the influence of different logical monitoring methods on the anti-attack performance of the system is analysed.Finally,the experiment proves that the dynamic heterogeneous redundancy structure composed of encryption logic monitoring can guarantee the safe and stable operation of the safety computer more effectively.

集成ISM与G1的建筑工人安全能力影响因素研究

为探究影响建筑工人安全能力的因素,提出一种集成解释结构模型(ISM)与序相关法(G1-Method)的因素分析法。首先,基于壳层模型(SHELL)与因子分析法,归纳与提取影响因素;其次,通过ISM构建工人安全能力影响因素多级递阶结构模型;最后,结合改进的G1-Method,计算因素间关联度及对安全能力的影响重要度。结果表明:所构建的安全能力影响因素结构模型包括安全认知能力、安全行为能力2个维度,以及16个影响因素。其中,安全观念、操作技能、环境适应是建筑工人安全能力形成的浅层因素,而安全教培、安全管理是安全能力形成的深层因素。同时,安全观念、安全教培、环境适应是安全认知能力的主要影响因素;操作技能、安全教培、安全管理是安全行为能力的主要影响因素。

基于企业安全生产双重预防机制的左领结图分析法研究与应用

为加强工业企业双重预防机制建设,将双重预防机制中的风险分级管控措施和隐患排查治理措施与事故减轻消除措施结合,通过分析事故逻辑创建Left-Bowtie分析模型,并根据该模型创新性地提出对企业双重预防机制建设及事故减轻消除措施进行安全评价的左领结图分析法。该方法首先通过风险辨识确定各风险点,建立风险屏障链,整合同一顶事件的各风险点形成完整的分析模型;然后根据建立的Left-Bowtie分析模型选取评价指标,建立评价指标体系,从而对顶事件的各项措施的安全性进行定量评价;最后根据评价结果提出针对性的整改方案。以某化工企业生产车间甲醇储罐泄漏事故为例,应用左领结图分析法对该企业安全生产中的双重预防机制进行了安全性分析。实例分析结果表明:左领结图分析法能够用于工业企业的安全风险管理,推进企业双重预防机制体系的建设,为企业安全生产水平的改进和提升明确方向和提供保障。