System of verification and solution of satisfiability modulo theory (SMT)-based fault tree and method thereof

Abstract

The invention relates to the technical field of computer software, and particularly to a system of verification and solution of a satisfiability modulo theory (SMT)-based fault tree and a method. Thesystem of verification and solution of the satisfiability modulo theory-based fault tree includes: the fault tree described by a formalized language of the satisfiability modulo theory; a formalized verification tool, namely an SMT solver which receives and verifies formalized logical formulas input into the fault tree, checks correctness thereof, and gives an error report; and a satisfiability modulo theory-based mini cut set (MCS) solution method which gives a mini cut set condition, gives a constraint condition at the same time to constrain output cut sets, outputs the number of elements ofthe output mini cut sets according to a user requirement size, and solves the problem of dependence of mini cut set calculation on a node order. A method, based on the satisfiability modulo theory ofthe above-mentioned system, of verification and solution of the mini cut sets is also included. According to the system, the satisfiability modulo theory can be used to carry out formalized verification on the fault tree, and correctness of a model is guaranteed.

Description

technical field [0001] The invention relates to the technical field of computer software, in particular to a fault tree verification and solution method, in particular to a fault tree verification and solution system and method based on a satisfiable model theory. Background technique [0002] Technological advances in many systems (including aircraft or other systems, such as those in the aerospace, automotive, marine, medical, and electronics industries) have led to rapid increases in complexity, and the reliability certification process for these systems requires one or more sub- Failure or fault analysis of a system, which is usually performed manually by a systems analyst. As complex systems and the systems of which they are composed become more integrated, traditional analysis methods can face reliability challenges due to many complexities in terms of the breadth of coverage and labor costs involved. [0003] Fault tree models are often used during the design, develo...

AI Technical Summary

Problems solved by technology

[0012] Methods and tools for developing and analyzing fault tree models often use general-purpose computer programming languages, so there are two problems to be solved or improved as mentioned above: there is no effective and convenient method to ensure the correctness of the fault tree itself; The process itself also needs a lot of checking calculations to ensure the correctness of the calculation results; general language and the current computer resources, there is no effective way to solve the permutation and combination explosion problem. Generally speaking, some method is used to obtain an approximate solution. That is to say, some minimum cut sets may be discarded in the approximation process

Images