Date of Award

12-1995

Document Type

Thesis

Degree Name

Master of Science

Department

Department of Electrical and Computer Engineering

Abstract

The understandability of object-oriented design techniques and the rigor of formal methods have improved the state of software development; however, both ideas have limitations. Object-oriented techniques, which are semi-formal, can still result in incorrect designs, while formal methods are complex and require an extensive mathematical background. The two approaches can be coupled, however, to produce designs that are both understandable and verifiable, and to produce executable code. This research proposes an approach where object-oriented models are first represented algebraically in a formal specification language such as LARCH and then transformed into a canonical form suitable for design refinement. In the canonical form presented in this work, object-oriented models are represented as domain theories consisting of multiple class specifications. Each class specification has sorts, operations (attributes, methods, events, states, state attributes, and operations), and axioms which describe its structure and behavior. The ability to reason about relationships between specifications is handled through the use of category theory operations. Although the canonical form is methodology independent, this work demonstrates the proposed approach on object-oriented models developed using Rumbaugh's Object Modeling Technique. The models are first mapped to LARCH and then translated into the canonical form by a set of rewrite rules. The rewrite rules are shown to produce unique normal forms. The final product is a transformation system which converts object-oriented designs into a canonical form that can be used with a design refinement tool.

AFIT Designator

AFIT-GCS-ENG-95D-01

DTIC Accession Number

ADA303748

Download

Share

COinS