A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiat...A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.展开更多
A nonlinear modeling framework is presented for an oceanographic unmanned aerial vehicle （UAV） by using symbolic modeling and linear fractional transformation （LFT） techniques . Consequently, an exact nonlinear sy...A nonlinear modeling framework is presented for an oceanographic unmanned aerial vehicle （UAV） by using symbolic modeling and linear fractional transformation （LFT） techniques . Consequently, an exact nonlinear symbolic LFT model of the UAV is derived in a standard M-A form where M represents the nominal, known, part of the system and A contains the time-varying, uncertain and nonlinear components. The advantages of the proposed modeling approach are that： it not only provides an ideal starting point to obtain various final design-oriented models through subse- quent assumptions and simplifications, but also it facilitates the control system analysis with models of different levels of fidelity/complexity. Furthermore, a linearized symbolic LFT model of the UAV is proposed based on the LFT differentiation, which is amenable directly to a sophisticated linear ro- bust control strategy such as μ synthesis/analysis. Both of the derived LFT models are validated with the original nonlinear model in time domain. Simulation results show the effectiveness of the pro- posed algorithm.展开更多
Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this pap...Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this paper we first present how quantified Boolean decision procedures can replace BDDs. We introduce a bounded model checking procedure for temporal logic CTL＊ which reduces model checking to the satisfiability of quantified Boolean formulas. Our new technique avoids the space blow up of BDDs, and extends the concept of bounded model checking.展开更多
基金Supported by the Natural Science Foundation of Guizhou Province(No.20050119)the Natural Science Foundation of Guizhou Education(No.2004219)
文摘A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.
文摘A nonlinear modeling framework is presented for an oceanographic unmanned aerial vehicle （UAV） by using symbolic modeling and linear fractional transformation （LFT） techniques . Consequently, an exact nonlinear symbolic LFT model of the UAV is derived in a standard M-A form where M represents the nominal, known, part of the system and A contains the time-varying, uncertain and nonlinear components. The advantages of the proposed modeling approach are that： it not only provides an ideal starting point to obtain various final design-oriented models through subse- quent assumptions and simplifications, but also it facilitates the control system analysis with models of different levels of fidelity/complexity. Furthermore, a linearized symbolic LFT model of the UAV is proposed based on the LFT differentiation, which is amenable directly to a sophisticated linear ro- bust control strategy such as μ synthesis/analysis. Both of the derived LFT models are validated with the original nonlinear model in time domain. Simulation results show the effectiveness of the pro- posed algorithm.
文摘Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this paper we first present how quantified Boolean decision procedures can replace BDDs. We introduce a bounded model checking procedure for temporal logic CTL＊ which reduces model checking to the satisfiability of quantified Boolean formulas. Our new technique avoids the space blow up of BDDs, and extends the concept of bounded model checking.
