I think it is a good idea to express the rules in the specification language for interface checking (of C) (SLIC), introduced in [1]. This approach has several advantages. Kernel developers usually have a good knowledge of C language. SLIC has a C-like syntax, so the entrance barrier for the developers is low. SDV tool translates API usage rules into C code due to Windows kernel-mode drivers being written in C. Thus, providing rules in a C-like language makes this translation easy.

Starting with Windows XP, Windows Driver Foundation (WDF) driver model supports both user-mode and kernel-mode drivers. User mode drivers can be written in languages, different from C. In order to support verification of such drivers, the SDV tool has to be extended. The verifier has to support translation from the API rules description language, into the target driver languages. It is also possible to use for the rules definition any language, other than SLIC, but expressive enough to define a state machine.

Since developers are rarely experts in formal methods, it would be too naїve to expect them submitting only the correct rules. That is why in my opinion the API ruleset building process cannot be fully automated and the control over the changes going into the production ruleset is necessary. I see such control done by a small group of maintainers of the ruleset – experts in the field of drivers verification tools.

Construction of the API ruleset starts with the initial ruleset, which can be based on the specifications obtained from the API's documentation. Then the ruleset should be extended and refined using the information, provided by the developers. The situations are possible when the new submitted rule:

1. extends the existing ruleset without overlapping. We mark the extended ruleset as a candidate for the testing;
2. overlaps with some rules from the existing ruleset. We have to merge the ruleset and the rule. This is equal to merging state-machines. We mark the merged ruleset as a candidate for testing;
3. contradicts some rules from the ruleset. We have to decide if the problem is in the ruleset or in the rule. We construct a new ruleset by adding the new rule to the non-contradicting part of the original ruleset and mark it for testing.

Now, we check the candidates for testing. We would like to know whether the new ruleset helps to find new bugs in the drivers, or hides the ones, that were discovered before. For this purpose we may use: a) a benchmark driver with a known number and type of errors in the APIs access or b) previous history of the drivers testing. In the case, when due to changes in the ruleset, some additional bugs are found and some previously discovered bugs are hidden, heuristic should be defined.

If the new ruleset passes the testing, we add the submitted rule as a candidate for the maintainers' review and further inclusion into the production ruleset. We also provide the developer and to the maintainers, with all the information, obtained during testing.

References
[1] T. Ball and S. K. Rajamani. SLIC: A specification language for interface checking. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.