Identification of missing properties in model checking

A verification processor, which is configured to receive an implementation model, defining model states of a target system and model transitions between the model states, and to receive a specification of the target system, including properties that the system is expected to obey, and which is operative to create a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties, and to compare the tableau transitions to the model transitions to determine whether a discrepancy exists therebetween.

A computer software product for verification of a specification of a target system, which specification includes properties that the system is expected to obey, by comparison with an implementation model, which defines model states of the target system and model transitions between the model states, the product comprising a computer-readable medium having computer program instructions recorded therein, which instructions, when read by a computer, cause the computer to create a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties, and to compare the tableau transitions to the model transitions to determine whether a discrepancy exists therebetween.

Model checking apparatus, which is configured to receive an implementation model, defining model states of a target system and model transitions between the model states, and to receive a specification of the target system, including properties that the system is expected to obey, and which is operative to create a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties, and to compare the tableau to the model by inputting the model and the tableau to an automatic model checking program.

A computer software product for verification of a specification of a target system, which specification includes properties that the system is expected to obey, by comparison with an implementation model, which defines model states of the target system and model transitions between the model states, the product comprising a computer-readable medium having computer program instructions recorded therein, which instructions, when read by a computer, cause the computer to create a tableau from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties, and to compare the tableau to the model by inputting the model and the tableau to an automatic model checking program.