Date of Award

12-1992

Document Type

Thesis

Degree Name

Master of Science

Department

Department of Electrical and Computer Engineering

First Advisor

Paul D. Bailor, PhD

Abstract

This research developed and implemented an automated technique for translating informal specifications into formal, executable specifications. A unified Abstract Model (UAM) was developed to combine the information contained in Entity Relationship, State Transition, and Data Flow Models into a concise, object-based representation. The UAM forms the basis for defining a formal language, the Object Modeling Language (OML), used to capture the information contained in the UAM. By using OML, we were able to develop an automated translation process to convert informal specifications into executable, formal specifications. The Software Refinery Development Environment enabled us to easily develop a parser that translates an OML specification into an abstract syntax tree. A Translation Executive transforms the information contained in the abstract syntax tree into an executable, REFINE specification. The specifier can quickly validate the correctness of the informal specification by testing its behavior. Additionally, the automatically generated executable specification serves as a basis for formal software design and future development. Two examples, a home heating system and a library database, were used to validate this formalization and transformation process. Our results clearly show the complementary nature of informal and formal methods, and provides a significant step towards formalizing the software development process.

AFIT Designator

AFIT-GCS-ENG-92-04

DTIC Accession Number

ADA258901

Comments

The authors' Vita pages are omitted.

Download

Share

COinS