by Jutta Eusterbrock
Formal correctness and conformance with user needs are criteria to assess the quality of software. Automatic software generation from formal descriptions of user requirements by logical means is a promising approach to achieve correct software. However, one of the major problems is specifying in advance the requirements in a non-ambiguous, complete, correct and adequate way.
The intent of the SEAMLESS approach is to enhance the software production process by providing a knowledge based synthesis environment which supports cyclic phases of "Specification, Experimentation, Abstraction, Modification, Logical validation and Extraction for System Synthesis (SEAMLESS)." Interactive system synthesis is perceived as a non-linear, incremental knowledge acquisition process.
The formal foundation is a multi-layer framework for knowledge representation within the logic programming paradigm. It allows to apply a single notation and a coherent concept for describing various useful forms of knowledge, eg. domain data or software components, and supporting reasoning tasks, eg. knowledge acquisition, software construction or program optimisation. Further - from a practical point of view - it is highly desirable to have synthesis systems which assure the re-usability of components, flexibility and evolution. Hence SEAMLESS is implemented as an easily extensible workbench of re-usable encapsulated theories, which are interacting by well-defined interfaces and hierarchically organized.
Three abstraction layers - each of them is subdivided into data type and rule specifications in the format of typed horn clauses - are introduced. The layers refer to the specification of domain knowledge, generic domain abstractions and the specification of knowledge sources, eg. program components, respectively. Theories and program components are considered as typed objects, which can be constructed dynamically. According to the different abstraction layers, the data types are assigned sets of terms, formulas, and theories as universes. The interaction between object layers and metalayers is realized by "viewpoints," which instantiate abstract domain schemas by concrete domain theories. Problems to be solved are stated as theorems or metatheorems to be proven and submitted as queries. Constructive solutions are computed by inference-based methods.
Within this framework correct and operational specifications of data types, optimisation rules for logic programs, mathematical domain knowledge, and generic methods were derived. Based on the specified data types and methods, the current implementation provides - among others - the following features:
The system is implemented in Prolog with a Tcl/Tk-based graphical user interface. A former version was applied for the discovery of a previously unknown, complex mathematical algorithm in the domain of partial-order sorting. Search complexities were tackled by extended strategic knowledge, which was implemented as annotated expert knowledge and automatically augmented at runtime by machine learning procedures.
Currently, the system is extended to provide an environment supporting the configuration of workstation/PC-based telecommunication systems which are customized to meet application specific requirements. System configurations are composed of hard- or software components, and deliver services, eg. fax or on-line services that connect to public telecommunication networks. The requirements taken into account consist of constraints on individual components and services as well as specifications of data, temporal, or preference dependencies between components.
gmd.de