Formal verification for distributed real-time control: periodic Producer/Consumer

The Producer/Consumer (P/C) has been used to model communication in networks. The model states that in a system there is a producer of a given information and one or more consumers of this information. With this model different kinds of communication failures may occur. In this paper with the help of the adapted synchronous model (ASM), we show two methods for formally verifying the necessary conditions to avoid buffer overwrites in the P/C model. Specifically, we explore the constraints on communication parameters in distributed periodic control and more generally, we demonstrate how behavioral properties can be analyzed using formal methods