SMT-Based Diagnosability For Real-Time Systems

With the rapid development of science and technology and artificial intelligence,intelligent large-scale complex systems have generally appeared in human production and life.In the course of system operation,no matter how large the size of the system,failure may occur,and small faults may cause incalculable losses.So in order to avoid this situation,fault diagnosis came into being.Fault diagnosis has always been a serious challenge and subject in complex automated control systems,its efficiency depends on the system characteristics,that is,diagnostics.Diagnosability determines the ability of a system to detect the occurrence of errors within a series of effectively observable sequences.Since the fault diagnosis was proposed,scholars have received extensive attention and research,and have achieved fruitful research results.A large number of documents make use of the Model-Based Diagnosis(MBD)method to analyze the diagnostics of the Discrete Event System(DES).In the MBD,the system's expected behavior can be derived,under the same input conditions,the actual behavior of the system can be monitored by arranging various sensors.Then the diagnostic results of the system can be obtained by comparing the expected behavior with the actual behavior.But so far,few researchers have studied the diagnostic capabilities of real-time systems(RTS),because in real-time systems,there are a lot of time constraints that make the system modeling difficult,but in reality,these time constraints,such as transmission delays,communication time,and response time,must be taken into account because they affect the diagnostics of the system and cannot be ignored in complex systems.In this paper,the problem is solved of bounded diagnosability in RTS by the method of MBD and diagnostic model theory(SMT).This paper mainly studies the bounded diagnosability problem in RTS from two aspects:First,considering the impact of time constraints on the system in a real-time system,the paper introduces a Timed Automata(TA)to model the real-time system.Timed automata was proposed by Alur and David in 1994.Time constraints are considered in the timed automata.It is the most widely used tool for studying real-time systems.In timed automata,the delay between different attribute events can be easily expressed.The paper adopts the MBD to model and analyze the RTS with a six-tuple TA,analogous to the diagnosability of discrete event systems,to redefine the concept of diagnostics in RTS,and also proves the system's diagnosability by defining the existence of time-critical pairs,then the paper illustrates the necessary and sufficient conditions for satisfying diagnosability in RTS and proves it.Secondly,the paper proposes a method based on Diagnosable Modulus Theory(SMT),this method is used to verify the bounded diagnosability of real-time systems on timed automata.In the SMT solver,the system diagnostic validity is mainly verified by coding the time automata and sufficient and necessary conditions that satisfy the system diagnostics.In the process of verifying the system with SMT,the necessary and sufficient conditions for satisfying diagnosability and system characteristics are subdivided into 12sub-rules according to different properties,and the paper defines the concept of equivalent paths,on which the system to be diagnosed is judged.In the specific determination process,the paper takes the condition of satisfying diagnosability as the background theoretical part in SMT,and takes the system to be diagnosed as an input to obtain the determination result.Finally,the paper sets up three groups of controlled experiments on the standard experimental benchmark HAVC system,the experiments choose the SMT solver z3 and use the control variable method.At last,the paper discusses the operation of the system under the condition of a single clock,multiple clocks and different scales,and analyzes the experimental time,memory usage and other conditions,and proves the feasibility and efficiency of the algorithm.