Automatic temporal verification of buffer systems

A formal model for processes that communicate through fifo message buffers is presented and a sound automatic proof system for verifying RTL definable properties of such systems is given and can be applied to some practical examples.

Abstract

In this paper we have presented a formal model for processes that communicate through fifo message buffers and have given a sound automatic proof system for verifying RTL definable properties of such systems. The proof method is modular. Although our method is not complete, we feel, as illustrated by the example, that it can be applied to some practical examples. Theorem 3.1 holds for any fragment L of temporal logic as long as the formulae in L do not distinguish between two computations one of which is a stuttered extension of the other. In this case, we can use our approach for proving properties given by formulae in L as long as the theory of fifo buffers in the logic L is decidable.