Applying Formal Verification Methods to Pure Rule-Based Programs

Reliability, defined as the guarantee that a program satisfies its specifications, is an important aspect of many applications for which rule-based expert systems are suited. Verification refer to the process used to determine the reliability of the rule-based program. Because past approaches to verification are informal, guarantees of reliability cannot fully be made without severely restricting the system. On the other hand, by constructing formal specifications for a program and showing the program satisfies those specifications, guarantees of reliability can be made. This paper presents an assertional approach to the verification of rule-based programs. The proof logical needed for verification is adopted from one already in use by researchers in concurrent programming. The approach involves using a language called Swarm, and requires one to express program specifications as assertions over the Swarm representation of the program. Among models the employ rule-based notation, Swarm is the first to have an axiomatic proof logic