A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ens...A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ensure system safety because any defect will have serious consequences. Model checking is a method for verifying system safety. In this paper, we propose the Dynamic Linear Hybrid Automaton (DLHA) specification language and show a method to analyze reachability for a system consisting of several DLHAs.展开更多
A useful life prediction method based on the integration of the stochastic hybrid automata(SHA) model and the frame of the dynamic fault tree(DFT) is proposed. The SHA model can incorporate the orbit environment, work...A useful life prediction method based on the integration of the stochastic hybrid automata(SHA) model and the frame of the dynamic fault tree(DFT) is proposed. The SHA model can incorporate the orbit environment, work modes, system configuration, dynamic probabilities and degeneration of components,as well as spacecraft dynamics and kinematics. By introducing the frame of DFT, the system is classified into several layers, and the problem of state combination explosion is artfully overcome.An improved dynamic reliability model(DRM) based on the Nelson hypothesis is investigated to improve the defect of cumulative failure probability(CFP), which is used to address the failure probability of components in the SHA model. The simulation using the Monte-Carlo method is finally conducted on two satellites, which are deployed with the same multi-gyro subsystem but run on different orbits. The results show that the predicted useful life of the attitude control system(ACS) with consideration of abrupt failure,degradation, and running environment is quite different between the two satellites.展开更多
Supervisory control and fault diagnosis of hybrid systems need to have complete information about the discrete states transitions of the underling system. From this point of view, the hybrid system should be abstracte...Supervisory control and fault diagnosis of hybrid systems need to have complete information about the discrete states transitions of the underling system. From this point of view, the hybrid system should be abstracted to a Discrete Trace Transition System (DTTS) and represented by a discrete mode transition graph. In this paper an effective method is proposed for generating discrete mode transition graph of a hybrid system. This method can be used for a general class of industrial hybrid plants which are defined by Polyhedral Invariant Hybrid Automata (PIHA). In these automata there are no resetting maps, while invariant sets are defined by linear inequalities. Therefore, based on the continuity property of the state trajectories in a PIHA, the problem is reduced to finding possible transitions between all two adjacent discrete modes. In the presented method, the possibility and the direction of such transitions are detected only by computing the angle between the vector field and the normal vector of the switching surfaces. Thus, unlike the most other reachability methods, there is no need to solve differential equations and to do mapping computations. In addition, the proposed method, with some modifications can be applied for extracting Stochastic or Timed Discrete Trace Transition Systems.展开更多
基于通信的列车运行控制(communication based train control,CBTC)系统采用车地通信方式使得地面设备极其复杂。随着通信技术的快速发展,以车载为核心的列车运行控制(train-centric communication based train control,TcCBTC)系统采...基于通信的列车运行控制(communication based train control,CBTC)系统采用车地通信方式使得地面设备极其复杂。随着通信技术的快速发展,以车载为核心的列车运行控制(train-centric communication based train control,TcCBTC)系统采用车车通信方式减少了控制信息的传递环节,将成为城市轨道交通领域的发展方向。移动授权(movementauthority,MA)是决定列车能否以安全间隔运行的直接因素,因此对MA生成过程进行形式化建模与分析,对避免列车碰撞具有重要意义。根据TcCBTC系统架构分析MA生成流程,确定参与功能实现的子系统,并计算出不确定性参数;通过UPPAAL-SMC建立对应的随机混成自动机网络模型;最后采用统计模型检测方法对模型进行定量分析。分析结果表明:置信度为99.95%的情况下,系统在300 ms内成功计算出MA的概率为0.9974124748,为后续TcCBTC系统开发设计提供理论参考。展开更多
电力线所处环境恶劣,工况复杂,具柔索特性,对巡线机器人的稳定性和可靠性提出较大挑战,因此以飞走巡线机器人(flying-walking power line inspection robot,FPLIR)为研究对象,提出了一种多模式切换混杂控制方法。在FPLIR巡检工作原理基...电力线所处环境恶劣,工况复杂,具柔索特性,对巡线机器人的稳定性和可靠性提出较大挑战,因此以飞走巡线机器人(flying-walking power line inspection robot,FPLIR)为研究对象,提出了一种多模式切换混杂控制方法。在FPLIR巡检工作原理基础上,建立4种控制模式的混杂自动机模型和相互切换的监测器模型;利用Lyapunov函数法和力角稳定性判据(force-angle stability margin,FASM)法分析FPLIR多模式切换和力学特性的稳定性;基于各模式的控制目标,提出了对应的控制策略,尤其结合FPLIR的结构和工况特点,设计变论域模糊控制器,提高FPLIR线上行走的稳定性,设计模型预测控制器,提高FPLIR落线的安全性。最后通过仿真和实验验证了多模式切换混杂控制方法的有效性和可行性,提升了FPLIR在复杂电力线环境下的适应性,为未来机器人智能巡检提供理论参考。展开更多
文摘A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ensure system safety because any defect will have serious consequences. Model checking is a method for verifying system safety. In this paper, we propose the Dynamic Linear Hybrid Automaton (DLHA) specification language and show a method to analyze reachability for a system consisting of several DLHAs.
基金supported by the Fundamental Research Funds for the Central Universities(2016083)
文摘A useful life prediction method based on the integration of the stochastic hybrid automata(SHA) model and the frame of the dynamic fault tree(DFT) is proposed. The SHA model can incorporate the orbit environment, work modes, system configuration, dynamic probabilities and degeneration of components,as well as spacecraft dynamics and kinematics. By introducing the frame of DFT, the system is classified into several layers, and the problem of state combination explosion is artfully overcome.An improved dynamic reliability model(DRM) based on the Nelson hypothesis is investigated to improve the defect of cumulative failure probability(CFP), which is used to address the failure probability of components in the SHA model. The simulation using the Monte-Carlo method is finally conducted on two satellites, which are deployed with the same multi-gyro subsystem but run on different orbits. The results show that the predicted useful life of the attitude control system(ACS) with consideration of abrupt failure,degradation, and running environment is quite different between the two satellites.
文摘Supervisory control and fault diagnosis of hybrid systems need to have complete information about the discrete states transitions of the underling system. From this point of view, the hybrid system should be abstracted to a Discrete Trace Transition System (DTTS) and represented by a discrete mode transition graph. In this paper an effective method is proposed for generating discrete mode transition graph of a hybrid system. This method can be used for a general class of industrial hybrid plants which are defined by Polyhedral Invariant Hybrid Automata (PIHA). In these automata there are no resetting maps, while invariant sets are defined by linear inequalities. Therefore, based on the continuity property of the state trajectories in a PIHA, the problem is reduced to finding possible transitions between all two adjacent discrete modes. In the presented method, the possibility and the direction of such transitions are detected only by computing the angle between the vector field and the normal vector of the switching surfaces. Thus, unlike the most other reachability methods, there is no need to solve differential equations and to do mapping computations. In addition, the proposed method, with some modifications can be applied for extracting Stochastic or Timed Discrete Trace Transition Systems.
文摘基于通信的列车运行控制(communication based train control,CBTC)系统采用车地通信方式使得地面设备极其复杂。随着通信技术的快速发展,以车载为核心的列车运行控制(train-centric communication based train control,TcCBTC)系统采用车车通信方式减少了控制信息的传递环节,将成为城市轨道交通领域的发展方向。移动授权(movementauthority,MA)是决定列车能否以安全间隔运行的直接因素,因此对MA生成过程进行形式化建模与分析,对避免列车碰撞具有重要意义。根据TcCBTC系统架构分析MA生成流程,确定参与功能实现的子系统,并计算出不确定性参数;通过UPPAAL-SMC建立对应的随机混成自动机网络模型;最后采用统计模型检测方法对模型进行定量分析。分析结果表明:置信度为99.95%的情况下,系统在300 ms内成功计算出MA的概率为0.9974124748,为后续TcCBTC系统开发设计提供理论参考。
文摘电力线所处环境恶劣,工况复杂,具柔索特性,对巡线机器人的稳定性和可靠性提出较大挑战,因此以飞走巡线机器人(flying-walking power line inspection robot,FPLIR)为研究对象,提出了一种多模式切换混杂控制方法。在FPLIR巡检工作原理基础上,建立4种控制模式的混杂自动机模型和相互切换的监测器模型;利用Lyapunov函数法和力角稳定性判据(force-angle stability margin,FASM)法分析FPLIR多模式切换和力学特性的稳定性;基于各模式的控制目标,提出了对应的控制策略,尤其结合FPLIR的结构和工况特点,设计变论域模糊控制器,提高FPLIR线上行走的稳定性,设计模型预测控制器,提高FPLIR落线的安全性。最后通过仿真和实验验证了多模式切换混杂控制方法的有效性和可行性,提升了FPLIR在复杂电力线环境下的适应性,为未来机器人智能巡检提供理论参考。
