In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the sa...In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.展开更多
This paper investigates the stability analysis and H_∞ control for a class of nonlinear timedelay systems,and proposes a number of new results.Firstly,an equivalent form is given for this class of systems by means of...This paper investigates the stability analysis and H_∞ control for a class of nonlinear timedelay systems,and proposes a number of new results.Firstly,an equivalent form is given for this class of systems by means of coordinate transformation and orthogonal decomposition of vector fields.Then,based on the equivalent form,some delay-dependent results are derived for the stability analysis of the systems by constructing a novel Lyapunov functional.Thirdly,the authors use the equivalent form and the obtained stability results to investigate the H_∞ control problem for a class of nonhnear time-delay control systems,and present a control design procedure.Finally,an illustrative example is given to show the effectiveness of the results obtained in this paper.It is shown that the main results of this paper are easier to check than some existing ones,and have less conservatism.展开更多
Control invariant sets play a key role in model predictive control.Using Lyapunov function,a technique is proposed to design control invariant sets of planar systems in a precise form.First,itis designed for a linear ...Control invariant sets play a key role in model predictive control.Using Lyapunov function,a technique is proposed to design control invariant sets of planar systems in a precise form.First,itis designed for a linear system in Brunovsky canonical form.Then,the result is extended to generallinear systems.Finally,the nonlinear control systems are considered,and some sufficient conditionsand design techniques are also obtained.Numerical examples are presented to illustrate the proposeddesign methods.展开更多
基金supported by the New Century Excellent Researcher Award Program from Ministry of Education of China (Grant No. NCET-07-0059)the Fundamental Research Funds for the Central Universities (Grant No.2011YJS006)+1 种基金the National High Technology Research and DevelopmentProgram of China ("863" Program) (Grant No. 2011AA010104)the State Key Laboratory of Rail Traffic Control and Safety Research Project(Grant Nos. RCS2008ZZ001, RCS2008ZZ005)
文摘In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.
基金supported by the National Natural Science Foundation of China under Grant Nos.G60774009,61074068,61034007,61374065,and 61304033the Research Fund for the Doctoral Program of Chinese Higher Education under Grant No.200804220028+1 种基金the Natural Science Foundation of Shandong Province under Grant Nos.ZR2013ZEM006,ZR2011EL021,BS2011ZZ012,2013ZRB01873Colleges and Universities in Shandong Province Science and Technology Project under Grant Nos.J13LN37 and J12LN29
文摘This paper investigates the stability analysis and H_∞ control for a class of nonlinear timedelay systems,and proposes a number of new results.Firstly,an equivalent form is given for this class of systems by means of coordinate transformation and orthogonal decomposition of vector fields.Then,based on the equivalent form,some delay-dependent results are derived for the stability analysis of the systems by constructing a novel Lyapunov functional.Thirdly,the authors use the equivalent form and the obtained stability results to investigate the H_∞ control problem for a class of nonhnear time-delay control systems,and present a control design procedure.Finally,an illustrative example is given to show the effectiveness of the results obtained in this paper.It is shown that the main results of this paper are easier to check than some existing ones,and have less conservatism.
基金supported by the National Natural Science Foundation of China under Grant Nos. 60674022, 60736022 and 60821091
文摘Control invariant sets play a key role in model predictive control.Using Lyapunov function,a technique is proposed to design control invariant sets of planar systems in a precise form.First,itis designed for a linear system in Brunovsky canonical form.Then,the result is extended to generallinear systems.Finally,the nonlinear control systems are considered,and some sufficient conditionsand design techniques are also obtained.Numerical examples are presented to illustrate the proposeddesign methods.
