Transforming Algebraically-Based Object Models into a Canonical Form for Design Refinement.
AIR FORCE INST OF TECH WRIGHT-PATTERSON AFB OH SCHOOL OF ENGINEERING
Pagination or Media Count:
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 Rumbaughs 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.
- Computer Programming and Software