{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/21013"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/21013","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Intelligent assistance in formalizing software specifications","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Miriyala, Kanth L."],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Harandi, Mehdi T."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-05-07T12:55:47Z","date_published":"2011-05-07T12:55:47Z","updated_at":"2026-07-22T22:25:17Z","subjects":["Artificial Intelligence","Computer Science"],"languages":["eng"],"rights":["Copyright 1991 Miriyala, Kanth L."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9136675","(UMI)AAI9136675"],"render_values":[{"text":"AAI9136675","href":null,"code":true},{"text":"(UMI)AAI9136675","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/21013","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Harandi, Mehdi T."]},{"key":"dc:creator","label":"Author","values":["Miriyala, Kanth L."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-05-07T12:55:47Z","10000-01-01","1991"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Artificial Intelligence","Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 1991 Miriyala, Kanth L."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9136675","(UMI)AAI9136675","http://hdl.handle.net/2142/21013"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Made available in DSpace on 2011-05-07T12:55:47Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9136675.pdf: 6691378 bytes, checksum: d99b1e77402f086768f28f513bf66876 (MD5) Previous issue date: 1991","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:47:53Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:21:39-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"]},{"key":"dc:title","label":"Title","values":["Intelligent assistance in formalizing software specifications"]}]}],"canonical_facts":{"dc:contributor":["Harandi, Mehdi T."],"dc:creator":["Miriyala, Kanth L."],"dc:date":["2011-05-07T12:55:47Z","10000-01-01","1991"],"dc:description":["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.","Made available in DSpace on 2011-05-07T12:55:47Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9136675.pdf: 6691378 bytes, checksum: d99b1e77402f086768f28f513bf66876 (MD5) Previous issue date: 1991","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:47:53Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:21:39-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"],"dc:identifier":["AAI9136675","(UMI)AAI9136675","http://hdl.handle.net/2142/21013"],"dc:language":["eng"],"dc:rights":["Copyright 1991 Miriyala, Kanth L."],"dc:subject":["Artificial Intelligence","Computer Science"],"dc:title":["Intelligent assistance in formalizing software specifications"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:17Z"}