Verification and solution system and method of fault tree based on satisfiable modulus theory

Abstract

The invention relates to the technical field of computer software, in particular to a fault tree verification and solution system and method based on a satisfiable model theory. The verification and solution system of the fault tree based on the satisfiable modulus theory, including the fault tree described in the formal language of the satisfiable modulus theory, the formal verification tool, namely the SMT solver, receives and verifies the formal logic formula of the input fault tree, and checks Its correctness, and gives an error report, and also includes the minimum cut set solution method based on the modulus theory that can be satisfied, given the minimum cut set condition, and at the same time given constraints to constrain the output cut set, the output of the minimum cut set will be The number of elements is output according to the size required by the user, which solves the problem that the calculation of the minimum cut set depends on the order of nodes. It also includes a method for verifying and solving the minimum cut set that can satisfy the modulus theory based on the above system. The present invention can use the model theory SMT to formally verify the fault tree to ensure the correctness of the model.

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