The Abstract Event-B Development Sample Clauses

The Abstract Event-B Development. In our first model we introduce processes, channels and data. We de- fine carrier sets for the set of processes PROCESS, the set of channels CHANNEL, and set of data blocks represented by Block. A block of data is a function of packet identifiers to data, Block = PKTID → DATA. Process objects are represented by a variable proc, and channels are rep- resented by a variable chan. Each process has a local buffer called bu f f , and channels hold data in a buffer called data. INVARIANTS proc ⊆ PROCESS chan ⊆ CHANNEL data ∈ chan→ Block bu f f ∈ proc→ Block The Write event models the writing of a block of data b to a channel. The parameters include the writing process p, and the target channel c. In addition to these parameters an additional local parameter b is introduced to keep track of the block of data to be written from the local buffer, where b = bu f f (p). Write ¾ ANY p, c, b WHERE p ∈ proc ∧ c ∈ chan ∧ b = bu f f (p) ∧ bu f f (p) =ƒ ∅ ∧ data(c) = ∅ THEN data(c) := b ǁ bu f f (p) := ∅ END The block b is copied to the data buffer data(c) and the local buffer