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. |
One-Pagers >