Critical computer program source code analyzing method for e.g. nuclear power plant, involves verifying hypothesis, and iterating verification operation until all hypotheses are analyzed, where verified hypothesis is marked as valid

摘要

The method involves transmitting a hypothesis on the validity of a property in a program point (L1) towards a centralizer module (21) by a front analyzer (F1), where the module stores the hypothesis in a hypotheses base (22) with an attribute indicating its origin analyzer and a status indicating that the hypothesis has to be verified. The hypothesis, stored in the base is verified, in which a rear analyzer (B1) is selected to analyze the hypothesis. Verification operation is iterated until all the hypotheses stored in the base are analyzed, where the verified hypothesis is marked as valid. An independent claim is also included for a system for verifying a source code of a computer program, comprising a front analyzer.