The design of intelligent control systems has become an area of intense research interest. The development of an effective methodology for the design of such control systems undoubtedly requires the synthesis of many ...The design of intelligent control systems has become an area of intense research interest. The development of an effective methodology for the design of such control systems undoubtedly requires the synthesis of many concepts from artificial intelligence. The most commonly used controller in the industry field is the proportional-plus-integral-plus-derivative (PID) controller. Fuzzy logic controller (FLC) provides an alternative to PID controller, especially when the available system models are inexact or unavailable. Also rapid advances in digital technologies have given designers the option of implementing controllers using Field Programmable Gate Array (FPGA) which depends on parallel programming. This method has many advantages over classical microprocessors. In this research, A model of the fuzzy PID control system is implemented in real time with a Xilinx FPGA (Spartan-3A, Xilinx Company, 2007). It is introduced to maintain a constant speed to when the load varies.,The model of a DC motor is considered as a second order system with load variation as a an example for complex model systems. For comparison purpose, two widely used controllers “PID and Fuzzy” have been implemented in the same FPGA card to examine the performance of the proposed system. These controllers have been tested using Matlab/Simulink program under speed and load variation conditions. The controllers were implemented to run the motor as real time application under speed and load variation conditions and showed the superiority of Fuzzy-PID.展开更多
Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP,...Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP, which is based on the timed automata (TA) theory. By devising RFID locating application into complex events, we model the timing diagram of RFID data streams based on the TA. We optimize the constraint of the event streams and propose a novel method to derive the constraint between objects, as well as the constraint between object and location. Experiments prove the proposed method reduces the cost of RFID complex event processing, and improves the efficiency of the RTLS.展开更多
Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a...Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a fair timed automaton （TA） that recognizes its satisfying models with prototype verification system （PVS） in this paper. Both the tabular construction＇s principles and the PVS implementation details are given for the different type of MITL formula according to the corresponding semantics interpretations. After this transformation procedure, specifications expressed with MITL formula can be verified formally in the timed automata framework developed previously.展开更多
Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although...Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.展开更多
基金supported by the Foundation for Innovative Research Groups of National Natural Science Foundation of China(No.51321065)the Foundation for Key Program of Natural Science Foundation of High Arch Dam(No.51339003)the National Basic Research Program of China(‘‘973’’Program,No.2013CB035904)
文摘The design of intelligent control systems has become an area of intense research interest. The development of an effective methodology for the design of such control systems undoubtedly requires the synthesis of many concepts from artificial intelligence. The most commonly used controller in the industry field is the proportional-plus-integral-plus-derivative (PID) controller. Fuzzy logic controller (FLC) provides an alternative to PID controller, especially when the available system models are inexact or unavailable. Also rapid advances in digital technologies have given designers the option of implementing controllers using Field Programmable Gate Array (FPGA) which depends on parallel programming. This method has many advantages over classical microprocessors. In this research, A model of the fuzzy PID control system is implemented in real time with a Xilinx FPGA (Spartan-3A, Xilinx Company, 2007). It is introduced to maintain a constant speed to when the load varies.,The model of a DC motor is considered as a second order system with load variation as a an example for complex model systems. For comparison purpose, two widely used controllers “PID and Fuzzy” have been implemented in the same FPGA card to examine the performance of the proposed system. These controllers have been tested using Matlab/Simulink program under speed and load variation conditions. The controllers were implemented to run the motor as real time application under speed and load variation conditions and showed the superiority of Fuzzy-PID.
文摘Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP, which is based on the timed automata (TA) theory. By devising RFID locating application into complex events, we model the timing diagram of RFID data streams based on the TA. We optimize the constraint of the event streams and propose a novel method to derive the constraint between objects, as well as the constraint between object and location. Experiments prove the proposed method reduces the cost of RFID complex event processing, and improves the efficiency of the RTLS.
基金Project supported by the National Natural Science Foundation of China （Grant Nos.60373072, 60673115）, the National Basic Research Program of China （Grant No.2002CB312001）, and the National High-Technology Research and Development Program of China （Grant No.2007AA012144）
文摘Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a fair timed automaton （TA） that recognizes its satisfying models with prototype verification system （PVS） in this paper. Both the tabular construction＇s principles and the PVS implementation details are given for the different type of MITL formula according to the corresponding semantics interpretations. After this transformation procedure, specifications expressed with MITL formula can be verified formally in the timed automata framework developed previously.
文摘Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.
文摘状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为.但目前STM不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用.针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画.此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明了上述方法的有效性.
