Construction And Application Of Hybrid Clock Logic Systen For Intelligent System

Intelligent system is the hotspot of current research.In some safety-critical intelligent systems,the time and space information must be consistent,that is,to reach the specific location at the specific time.In order to ensure the spatio-temporal consistency of intelli-gent systems,the time and space information of systems need to be specified.There are usually two types of clocks:physical clock and logical clock.The hybrid clock formed by combining the two can simultaneously specify physical clock and logical clock.The physical clock contains the space and time information of the intelligent system,which specifies the spatio-temporal consistency.We construct a hybrid clock logic(HCL)sys-tem to specify the spatio-temporal properties of the intelligent system.The HCL model checking is used to verify the properties of the system to ensure the safety and reliability of the system.The specific research contents are as follows1.We establish the syntax structure of hybrid clock logic.In order to meet the require-ments of the system properties description,we propose some new operations and relations based on the existing hybrid clock operations and relations,and define the syntax of HCL.Some concrete high-speed train examples are given to explain the hybrid clock operations and relations,and then we study the relevant properties of the hybrid clock relations2.We construct the model checking method of hybrid clock logic.Firstly,the seman-tics of HCL formulas are given by defining the satisfiable relationship between the spatio-temporal consistency language STeC design and the HCL formulas.Then,based on the hybrid clock converted from the STeC design for model checking,the HCL model checking algorithm is designed.Finally,case studies in the fields of high-speed train and aerospace show the effectiveness of HCL and the correctness of the model checking algorithm3.We design and develop the STeC model checking tool based on hybrid clock log-ic system.The tool can convert STeC design into hybrid clock,and verify the properties of the system described by the HCL formulas.The high-speed train and aerospace cases show the availability of the tool.