Formal Verification of Pure Production Systems 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. Executing rule-based programs on a series of test cases. To show a program is reliable, it is desirable to construct formal specifications for the program and to prove that it obeys those specifications. This paper presents an assertional approach to the verification of a class of rule-based programs characterized by the absence of conflict resolution. The proof logic needed for verification is already in use by researchers in concurrent programming. The approach involves expressing the program in a language called Swarm, and its specifications as assertions over the Swarm program. Among models that employ rules-based notation, Swarm is the first to have an axiomatic proof logic. A brief review of Swarm and its proof logic is given, along with an illustration of the formal verification method used on a simple rule-based program