Intelligent assistance in formalizing software specifications

A formal software specification expresses in a mathematically correct way what requirements the software should satisfy. It guides software design and code generation, forms a basis for software verification, and is a valuable documentation for code. However, the process of deriving software specifications from informal requirements is tedious, error-prone, time-consuming, and expensive. Hence automated support is needed to reduce the cost and improve the quality of software specifications.This thesis describes techniques that can be used in formalizing specifications. It presents a system, called SPECIFIER, incorporating these techniques, that assists the human requirements analyst in formalizing specifications. The user presents the informal requirements to the system in an interactive manner using a restricted subset of the natural language. We view the process of formalizing specifications as a problem-solving process. The system uses problem-solving techniques such as the use of schemas, analogy, and difference-based reasoning. If an informal description is a commonly occurring operation for which the system has a schema, then the formal specification is obtained by instantiating the schema. If there is no such schema, SPECIFIER tries to find a previously solved problem which is analogous to the current problem. If the problem found is in direct analogy with the current problem, it applies the associated analogy mapping to formalize the specification. On the other hand, if the analogy found is only approximate, it formalizes the directly analogous part of the problem by analogy, and then performs difference-based reasoning using the remaining (unmatched) parts to transform the partial formal specification obtained by analogy to a formal specification for the entire original problem.U of I OnlyETDs are only available to UIUC Users without author permissio