Formal Transformations from Graphically-Based Object-Oriented Representations to Theory-Based Specifications
AIR FORCE INST OF TECH WRIGHT-PATTERSON AFB OH
Pagination or Media Count:
Formal software specification has long been touted as a way to increase the quality and reliability of software however, it remains an intricate, manually intensive activity. An alternative to using formal specifications is to use graphically-based, semi-formal specifications such as those used in many object-oriented specification methodologies. While semi-formal specifications are generally easier to develop and understand, they lack the rigor and precision of formal specification techniques. The basic premise of this investigation is that formal software specifications can be constructed using correctness preserving transformations from graphically-based object-oriented representations. In this investigation, object-oriented specifications defined using Rumbaughs Object Modeling Technique OMT were translated into algebraic specifications. To ensure the correct translation of graphically-based OMT specifications into their algebraic counterparts, a formal semantics for interpreting OMT specifications was derived and an algebraic model of object-orientation was developed. This model defines how object-oriented concepts are represented algebraically using an object-oriented algebraic specification language O-SLANG. O-SLANG combines basic algebraic specification constructs with category theory operations to capture internal object class structure as well as relationships between classes. Next, formal transformations from OMT specifications to O-SLANG specifications were defined and the feasibility of automating these transformations was demonstrated by the development of a proof-of-concept system.
- Computer Programming and Software