Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a...Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a formal method with precise syntax and semantics defined. System modeled by PVS specification could be verified by tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time systems. In this approach, we provide 1) a time-extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from a timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexibility and user friendliness in modeling, extendability in formalization and verification content, and better performance. Time constraints are modeled and verified and is a highlight of this paper.展开更多
Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an ind...Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an industrial standard modeling language which provides a powerful expressi-veness, intuitive and easy to use interface to model. UML is widely accepted by software developer. However, for lack of precisely defined semantics, especially on the dynamic diagrams, UML model is hard to be verified. PVS is a general formal method which provides a high-order logic specification language and integrated with model checking and theorem proving tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time system. In this approach, we provide 1) a timed extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexible and friendly in modeling, extendable in forma-lization and verification content, and better performance. Time constraints are modeled and verified and it’s a highlight of this paper.展开更多
A method of real-time data smoothness which is applied in a hardware-in-the-loop （HIL） simulation platform for a plug-in hybrid electric vehicle synthetical power device is described. The input signal of the platfor...A method of real-time data smoothness which is applied in a hardware-in-the-loop （HIL） simulation platform for a plug-in hybrid electric vehicle synthetical power device is described. The input signal of the platform comes from a AC/DC switch power with output containing noises. A linear slide average arithmetic is applied to smooth the noises. To average a certain number input sample signals, this method can decrease the noises voltage level, which meet the requirement of the simulation platform. The efficiency and signal delay time are presented to describe the result of this method, and a statistical index is used to judge the arithmetic＇ s efficiency. The tests results show that the arithmetic fit the requirement of the HIL simulation platform.展开更多
In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the...In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the electricity price at each time. A PBN is widely used as a model of complex systems, and is appropriate as a model of real-time pricing systems. Using the PBN-based model, real-time pricing systems can be quantitatively analyzed. In this paper, we propose a verification method of real-time pricing systems using the PBN-based model and the probabilistic model checker PRISM. First, the PBN-based model is derived. Next, the reachability problem, which is one of the typical verification problems, is formulated, and a solution method is derived. Finally, the effectiveness of the proposed method is presented by a numerical example.展开更多
The article focuses on the influence of operator and process safety and the trends of robotics and digitalisation on a ladle slide gate that was introduced to the market 6 years ago[1].After more than 50 installations...The article focuses on the influence of operator and process safety and the trends of robotics and digitalisation on a ladle slide gate that was introduced to the market 6 years ago[1].After more than 50 installations,customer experience was gathered and new features were added to a system upgrade.These upgrades are related to safety,ease of operation,and low operational costs.Especially a newly introduced“open check”feature increases the confidence level of the operators and can boost performance.With growing requirements to increase safety for people and processes in the ladle preparation area and on the continuous casting floor,automation has become increasingly important in steel plants.A slide gate prototype is currently underway to launch an innovative new gate design striving for full automation.Several critical process steps are already available and successfully used in the steel plants,such as cylinder connection,slag detection integration,and ladle gate preparation area automation.Fully automated operation will be followed by digitalisation,allowing for tracking of performance,safety,and quality.This paper summarises new features available for slide gates and outlines individual initiatives towards fully automated operation and data acquisition examples of digitalisation.展开更多
In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is loca...In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.展开更多
The observation vectors in traditional coarse alignment contain random noise caused by the errors of inertial instruments,which will slow down the convergence rate.To solve the above problem,a real-time noise reductio...The observation vectors in traditional coarse alignment contain random noise caused by the errors of inertial instruments,which will slow down the convergence rate.To solve the above problem,a real-time noise reduction method,sliding fixed-interval least squares(SFI-LS),is devised to depress the noise in the observation vectors.In this paper,the least square method,improved by a sliding fixed-interval approach,is applied for the real-time noise reduction.In order to achieve a better-performed coarse alignment,the proposed method is utilized to de-noise the random noise in observation vectors.First,the principles of proposed SFI-LS algorithm and coarse alignment are devised.A simulation test and turntable experiment were executed to demonstrate the availability of the designed method.It is indicated that,from the results of the simulation and turntable tests,the designed algorithm can effectively reduce the random noise in observation vectors.Therefore,the proposed method can enhance the performance of coarse alignment availably.展开更多
Because of the widely-used nonlinear loads, the problems of harmonics and low power factor in power systems are becoming more and more serious. In view of the above problems, a shunt three-phase active power filter （...Because of the widely-used nonlinear loads, the problems of harmonics and low power factor in power systems are becoming more and more serious. In view of the above problems, a shunt three-phase active power filter （SAPF） based on discrete sliding mode control to suppress the harmonics was designed and the power factor improved. First, built the mathematical model of SAPF. Then, controlled the switch through analyzing the harmonic current that was controlled signal using discrete sliding mode control. Through simulation using MATLAB, verified the validity of the algorithm. By the simulation waveforms, it can be found that after the load current containing a large number of harmonics passes the active power filter, the waveform of the power current approximately becomes a sine wave and the harmonics is significantly reduced. As a result, it plays a good role in purifying power systems. Moreover, from the waveforms of harmonic current and power current, it can be found that the algorithm has a faster tracking speed. The waveform can fect.展开更多
In this paper,a predictive sliding mode control method based on multi-sensor fusion is proposed to solve the problem of insufficient accuracy in trajectory tracking caused by actuator delay.The controller,based on the...In this paper,a predictive sliding mode control method based on multi-sensor fusion is proposed to solve the problem of insufficient accuracy in trajectory tracking caused by actuator delay.The controller,based on the kinematics model,uses an inner and outer two-layer structure to achieve decoupling of position control and heading control.A reference positional change rate is introduced into the design of controller,making the automatic guided vehicle(AGV)capable of real-time predictive control ability.A stability analysis and a proof of predictive sliding mode control theory are provided.The experimental results show that the new control algorithm can improve the performance of the AGV controller by referring to the positional change rate,thereby improving the AGV operation without derailing.展开更多
文摘Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a formal method with precise syntax and semantics defined. System modeled by PVS specification could be verified by tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time systems. In this approach, we provide 1) a time-extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from a timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexibility and user friendliness in modeling, extendability in formalization and verification content, and better performance. Time constraints are modeled and verified and is a highlight of this paper.
文摘Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an industrial standard modeling language which provides a powerful expressi-veness, intuitive and easy to use interface to model. UML is widely accepted by software developer. However, for lack of precisely defined semantics, especially on the dynamic diagrams, UML model is hard to be verified. PVS is a general formal method which provides a high-order logic specification language and integrated with model checking and theorem proving tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time system. In this approach, we provide 1) a timed extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexible and friendly in modeling, extendable in forma-lization and verification content, and better performance. Time constraints are modeled and verified and it’s a highlight of this paper.
文摘A method of real-time data smoothness which is applied in a hardware-in-the-loop （HIL） simulation platform for a plug-in hybrid electric vehicle synthetical power device is described. The input signal of the platform comes from a AC/DC switch power with output containing noises. A linear slide average arithmetic is applied to smooth the noises. To average a certain number input sample signals, this method can decrease the noises voltage level, which meet the requirement of the simulation platform. The efficiency and signal delay time are presented to describe the result of this method, and a statistical index is used to judge the arithmetic＇ s efficiency. The tests results show that the arithmetic fit the requirement of the HIL simulation platform.
文摘In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the electricity price at each time. A PBN is widely used as a model of complex systems, and is appropriate as a model of real-time pricing systems. Using the PBN-based model, real-time pricing systems can be quantitatively analyzed. In this paper, we propose a verification method of real-time pricing systems using the PBN-based model and the probabilistic model checker PRISM. First, the PBN-based model is derived. Next, the reachability problem, which is one of the typical verification problems, is formulated, and a solution method is derived. Finally, the effectiveness of the proposed method is presented by a numerical example.
文摘The article focuses on the influence of operator and process safety and the trends of robotics and digitalisation on a ladle slide gate that was introduced to the market 6 years ago[1].After more than 50 installations,customer experience was gathered and new features were added to a system upgrade.These upgrades are related to safety,ease of operation,and low operational costs.Especially a newly introduced“open check”feature increases the confidence level of the operators and can boost performance.With growing requirements to increase safety for people and processes in the ladle preparation area and on the continuous casting floor,automation has become increasingly important in steel plants.A slide gate prototype is currently underway to launch an innovative new gate design striving for full automation.Several critical process steps are already available and successfully used in the steel plants,such as cylinder connection,slag detection integration,and ladle gate preparation area automation.Fully automated operation will be followed by digitalisation,allowing for tracking of performance,safety,and quality.This paper summarises new features available for slide gates and outlines individual initiatives towards fully automated operation and data acquisition examples of digitalisation.
文摘In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.
基金This work was supported in part by the Inertial Technology Key Lab Fund 614250607011709in part by the Fundamental Research Funds for the Central Universities 2242018K40065,2242018K40066in part by the Foundation of Shanghai Key Laboratory of Navigation and Location Based Services,Key Laboratory Fund for Underwater Information and Control 614221805051809.
文摘The observation vectors in traditional coarse alignment contain random noise caused by the errors of inertial instruments,which will slow down the convergence rate.To solve the above problem,a real-time noise reduction method,sliding fixed-interval least squares(SFI-LS),is devised to depress the noise in the observation vectors.In this paper,the least square method,improved by a sliding fixed-interval approach,is applied for the real-time noise reduction.In order to achieve a better-performed coarse alignment,the proposed method is utilized to de-noise the random noise in observation vectors.First,the principles of proposed SFI-LS algorithm and coarse alignment are devised.A simulation test and turntable experiment were executed to demonstrate the availability of the designed method.It is indicated that,from the results of the simulation and turntable tests,the designed algorithm can effectively reduce the random noise in observation vectors.Therefore,the proposed method can enhance the performance of coarse alignment availably.
基金Supported by the National Natural Science Foundation of China （50375026, 50375028）
文摘Because of the widely-used nonlinear loads, the problems of harmonics and low power factor in power systems are becoming more and more serious. In view of the above problems, a shunt three-phase active power filter （SAPF） based on discrete sliding mode control to suppress the harmonics was designed and the power factor improved. First, built the mathematical model of SAPF. Then, controlled the switch through analyzing the harmonic current that was controlled signal using discrete sliding mode control. Through simulation using MATLAB, verified the validity of the algorithm. By the simulation waveforms, it can be found that after the load current containing a large number of harmonics passes the active power filter, the waveform of the power current approximately becomes a sine wave and the harmonics is significantly reduced. As a result, it plays a good role in purifying power systems. Moreover, from the waveforms of harmonic current and power current, it can be found that the algorithm has a faster tracking speed. The waveform can fect.
基金This work was supported by the National Natural Science Foundation of China(Grant Nos.61903241,61304223,61603191,61873158,61573237)the China Postdoctoral Science Foundation(Grant No.2018M630424)the Natural Science Foundation of Shanghai Municipality(Grant No.18ZR1415100).
文摘In this paper,a predictive sliding mode control method based on multi-sensor fusion is proposed to solve the problem of insufficient accuracy in trajectory tracking caused by actuator delay.The controller,based on the kinematics model,uses an inner and outer two-layer structure to achieve decoupling of position control and heading control.A reference positional change rate is introduced into the design of controller,making the automatic guided vehicle(AGV)capable of real-time predictive control ability.A stability analysis and a proof of predictive sliding mode control theory are provided.The experimental results show that the new control algorithm can improve the performance of the AGV controller by referring to the positional change rate,thereby improving the AGV operation without derailing.
