Formalization and Transformation of Informal Analysis Models into Executive REFINE (trademark) Specifications
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 bv 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1992
- Accession Number
- ADA258901
Entities
People
- Bradley D. Mallare
- Mary M. Boom
Organizations
- Air Force Institute of Technology