This work is concerned with the automation of the software specification process. Specification automation research to date has concentrated on non-interacting tlanslition of complete, correct, but informal problem descriptions into formal specifications. The work proposed here is unique in that it addresses the construction of complete, correct informal problem descriptions from incomplete, often incorrect user descriptions. The proposed system will rely on interactive problem solving and large amounts of domain specific knowledge to carry out this process.
Our work centers on a system that interacts with a user to elicit the details of a problem in a specific domain. It attempts to incorporate certain skills found in expert, human, domain analysts. These include 1) the ability to refine a sketchy, incomplete problem description into a complete form, 2) the ability to recognize known examples during problem acquisition, and 3) the ability to critique a user's description in terms of missing detail and lack of coverage. To realize these skills, we propose using the problem solving system Glitter to represent refinement knowledge, a combination of frames and state-transition diagrams to model the domain itself, and the ORBS rule-based system to implement knowledge-based symbolic evaluation.
Finally, the system will automatically translate (i.e., compile) the informal problem description into a formal specification. Our current target is the Gist specification language, although other languages are under consideration.