One-Pagers‎ > ‎

OP5: A Service for Specifying API Rules

Writing useful specifications is challenging and usually requires specialized knowledge not only of the target domain but also of the verification technology being used. Since developers are rarely experts in formal methods, we would like to automate this process as much as possible. This OP is concerned with synthesizing precise specifications from multiple approximate specifications. 

Assume you are part of the SDV team at the beginning of the project for deriving API rules. Instead of using manual processing of the information from Microsoft developers, you want to automate the entire process. To accomplish this, you develop an internal web service where developers can go and input their knowledge of the kernel/driver API; the web service then takes the input from the various developers, processes it, and produces the 60 API rules described in the SDV paper.

Describe how you would develop such a system. Pay particular attention to the language that developers use to input the information, the toolchain behind the web service, and the language in which the final API rules are stated.