A research project in applying formal methods at The Boeing Company, Seattle, Washington, USA is investigating category-theoretic methods for knowledge-based systems development and automated software synthesis.

Using The Kestrel Institute's Specware (TM) package (see publications and an index), investigators are experimenting with the automated synthesis of detailed software specifications from simple, abstract component specifications, and the automated translation of specifications into programs in a target programming language.

In doing this mathematically, the specifications are formalized as finite presentations of theories in a formal logic. Pairs of specifications are related through mathematical relationships called specification morphisms, which ensure that provable statements in one theory are representable as provable statements in the other. Diagrams of specifications and specifications morphisms represent a complex of interrelated theories about an application (for example, theories of manufacturing, material properties, and geometry are interrelated in manufacturing airplane parts). An algorithm for finding colimits of these diagrams is applied to synthesize detailed specifications that embody the specifications and relationships expressed in the diagrams.

In this way, knowledge about an application, expressed mathematically (through categorical logic) is built up in a sequential/parallel refinement process to produce mathematically verified specifications for software. Software is then produced through categorical mappings that transform theories from one logic to another (i.e., from the specification logic to a formally-defined version of a programming language). Categorical concepts in addition to colimits, such as functors and natural transformations, and sheaf-theoretic concepts that express commonality between specifications in a diagram, are fundamental parts of this process.

*This document does not represent an official position of The Boeing Company or any of its subsidiaries or suppliers.