| 摘要 |
An apparatus and method for verifying system behavior using behavior-constraint-calculus analysis is disclosed. The apparatus accepts a first "known" constraint graph and a second "conjectured" constraint graph. The apparatus transforms the second graph in such a way that the resultant "verified" graph "accepts" only those paths that are implied by the first graph and appear in the second graph. |
