Per group verification

摘要

Various embodiments provide per group verification techniques in which code may be verified against one or more rules on a group by group basis. In one or more embodiments relationships between portions of a module to be verified can be defined. By being aware of relationships between various code portions, various embodiments can divide a module into related groups and perform verification on the basis of the groups. Multiple groups can be derived based at least in part upon the relationships. Each group can then be verified separately for compliance with one or more rules. Verification results can be output for each of the groups.

主权项

1. A computer-implemented method comprising:
ascertaining multiple pathways in code to be verified by referencing a harness file that designates a position of callbacks within the code relative to a non-deterministic portion of the code defined by one or more non-deterministic choices, harness designations being sufficient to identify the multiple pathways; forming groups for verification of the code according to identified pathways, each of the groups containing a portion of the code to be verified; and directly verifying the code against one or more rules using the formed groups, including:
for a first rule:
executing respective pathways in the code corresponding to each of the groups; andmonitoring to determine compliance of the respective pathways with the first rule; andwhen the code is verified against multiple rules, for each other said rule:
executing the respective pathways in the code corresponding to each of the groups; andmonitoring to determine compliance of the respective pathways with the other said rule.