The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #730

Title:Layered Design of Kbs from Specification to Hardware
Authors:Robertson,DS; Park,N; Agusti,J
Date:Jan 1995
Presented:Presented at the ECAI-94 Workshop on Formal Methods for Knowledge-Based Systems
Keywords:
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 implementation and 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 predict 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 translation 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 in 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.
Download:POSTSCRIPT COPY

[Search These Pages] [DAI Home Page] [Comment]