SPECWARE, An Advanced Software Development Environment

We will design and build SPECWARE, an advanced software development environment for specifying, designing, and evolving high-performance, correct-by-construction software. Software development using SPECWARE will consist of the systematic transformation of formal specifications into executable programs, using high-level design steps formally represented within the system. The emphasis will be towards automating the design process by formally representing all processes and products relevant to design. This, in turn, will support iterative design and the integration of evolution with design. SPECWARE will be a "shrink/wrapped" tool, commercial off-the-shelf software that comes complete with manuals, books, and training classes. The tool will be roughly analogous to a hardware design workstation for VLSI, but based on a solid theoretical foundation for software design. SPECWARE will be based on a small set of powerful core concepts, logical theories (knowledge modules), morphisms between theories (translation between modules), and colimits (composition of modules) which have been implicitly present in several research prototypes at Kestrel Institute, most notably the KIDS and DTRE systems. The work involved in producing the SPECWARE tool is the redesign of our current synthesis environment into a more open, robust, extensible, scalable, customizable, and usable architecture.