I.D. Craig, Formal Specification of AI Systems: Four Case Studies (March 1, 1991).
In this paper, we outline four AI systems and their formal specification in Z. Two of the systems (a blackboard framework and the author's CASSANDR architecture) are of high complexity and are for predominantly real-time, high reliability applications; the other two are production systems of an unconventional type. The first production system (called ELEKTRA) contains extensive facilities for performing meta-level inference. The second extends ELEKTRA with a frame system and organises rules into rulesets for enhanced modularity (its specification is still underway). Both production systems contain control features that can be accessed by rules: both are reflective systems. To date, the four specifications amount to more than 500 A4 pages, including proofs and explanatory text. The four specifications are related in that solutions to the problems encountered in the blackboard and CASSANDRA systems are attempted in the other two specifications. The formal specifications of the second two systems were undertaken because we wanted to experiment with ideas without having to engage in implementation at too early a stage ( ELEKTRA was subsequently implemented in Scheme from its Z specification): this turned out to be an excellent strategy. To conclude the paper, we review our approach and consider the general use of formal specifications in the development of AI systems.