Edinburgh Research Explorer

Layered Design of KBS from Specification to Hardware

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Original languageEnglish
Title of host publicationProceedings of ECAI workshop on formal specification of knowledge-based systems
Number of pages15
Publication statusPublished - 1994

Abstract

Knowledge based systems are now being embedded within the hardware of household items, such as cameras and washing machines. These systems demand a high degree of reliability, both in terms of the components used in implementationand in ensuring that the initial specification of the system is accurately implemented. We examine this problem in the context of a standard KBS specification language: first order predicate calculus (FOPC). Two key problems emerge. The first is to provide a reliable bridge between the axioms of FOPC and the design required for hardware implementation. If our FOPC specification can be translated to an equivalent propositional axiom set then we can provide an automatic transtation to existing design languages (e.g. functional logics). However, most KBS specifications cannot be simplified in this way. By drawing on work from a hitherto unrelated area we demonstrate, by example, how a significant class of non-propositional FOPC axioms can be translated automatically to an implementation level design language. The second problem is keeping track of the gradual process of refinement necessary when moving from an initial, underspecified description to the restricted class of FOPC appropriate for automatic translation to an implementation design. We describe a layered system of formal specification which permits incremental specification of the design and enables designers to converge on the appropriate class of FOPC axioms.

ID: 3507571