Intelligent assistance in formalizing software specifications
Miriyala, Kanth L.
This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/21013
Description
Title
Intelligent assistance in formalizing software specifications
Author(s)
Miriyala, Kanth L.
Issue Date
1991
Doctoral Committee Chair(s)
Harandi, Mehdi T.
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Artificial Intelligence
Computer Science
Language
eng
Abstract
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
