Formal Verification Of Temporal Constraint Activity Anomaly Monitoring System Based On Timed Automata

Internet of Things is considered to be the third wave of information industry following computers,the Internet and mobile communications networks.in order to achieve purposes of intelligent identification,positioning,tracking and management,Internet of things use the sensor devices to obtain "entity" information,and use the network to make information exchange.The workshop production process abnormal state monitoring system based on the Internet of things became more and more in recent years,the system collect the production workshop data and analysis them,which will help the enterprises achieve intelligent workshop management and improve the economic interests of enterprises.However,in the production workshop monitoring system,involved in the object of information interaction,including people,machines,objects and other different types of objects,leading to the "user" of the pansex,the systems need to deal with a large number of heterogeneous information,more seriously,with the expansion of the processing scale,monitoring logic will become complex,it could not be guaranteed that the monitoring system fully meet the design requirements.Therefore,it is necessary to model and verify the production workshop monitoring system by using the formal method before the implementation of the system,and it is essential to find out the unreasonable and incorrect system design as soon as possible.Timed Automata provides a simple and effective way to describe real-time system state transition graphs with strong temporal expression capabilities,providing a formal approach to real-time system behavior modeling and performance analysis.Based on the research of production workshop anomaly monitoring system,this paper studied the formal verification method of temporal constraints activity anomaly monitoring based on time automata,and in order to find out the validity and completeness of the monitoring system by adopting the advantages of time automata in verification.In this paper,the research status of complex events detection at home and abroad reviewed.The characteristics of the workshop were summarized,the models of the production workshop site based on time automata were defined,and the randomness of the operator was described by the time constraint in the state invariant,different types of activities were portrayed by the state and the transition,at the same time,the different types of perceived behavior of the production object were abstracted;Then the different events patterns by different usage method and consumption strategy were illustrated,The method of constructing the event and event constraint model was illustrated,and a time automaton model construction method was proposed in which the composite event mode adopts several time constraint related event operators.The control model time automata modeling method was proposed,and the control model reduced the scale of automaton model corresponded to complex event pattern;Then,in order to simplify the verification of the nature of the anomaly monitoring time automata model,an automatic machine model of auxiliary production process with normal production was established.In view of the characteristics of the abnormal monitoring system in the production workshop,the correctness and completeness of the monitoring system designed were deduced from four aspects: system function,real-time,redundancy and undefined behavior.Finally timed automata authentication tool UPPAAL was used,the gluing processing workshop monitoring system as an example,the proposed method was validated.The research showed that: timed automata formalism method can better describe production workshop abnormal monitoring system related features.Using the formal modeling and verification of timed automata method can effectively find monitoring system for potential problems,to a certain extent,the auxiliary monitoring system development and design provide a basis for effective improvement in related personnel.The experimental results show that the proposed method has certain application value and significance.