• Ingen resultater fundet

Formal Specification of Distributed Systems:Communicating Sequential Processes (CSP)

N/A
N/A
Info
Hent
Protected

Academic year: 2022

Del "Formal Specification of Distributed Systems:Communicating Sequential Processes (CSP)"

Copied!
10
0
0

Indlæser.... (se fuldtekst nu)

Hent nu ( 10 Sider )

Hele teksten

(1)

DTU Informatics

Department of Informatics and Mathematical Modelling

Formal Specification of Distributed Systems:

Communicating Sequential Processes (CSP)

Nicola Dragoni

Embedded Systems Engineering DTU Informatics

Pipes

(2)

DTU Informatics

Department of Informatics and Mathematical Modelling

Pipes

• Processes with only two channels in their alphabet, namely an input channel left and an output channel right are called pipes.

2

(3)

DTU Informatics

Department of Informatics and Mathematical Modelling

Joining Pipes

• The processes P and Q may be joined together (P >> Q) so that

‣ the right channel of P is connected to the left channel of Q, and

‣ the sequence of messages output by P and input by Q on this internal channel is concealed from their common environment.

(4)

DTU Informatics

Department of Informatics and Mathematical Modelling

Connection Diagram

• This connection diagram represents the concealment of the connecting channel by not giving it a name.

• It also shows that

‣ all messages input on the left channel of (P>>Q) are input by P

‣ all messages output on the right channel of (P>>Q) are output by Q.

• Finally (P>>Q) is itself a pipe, and may again be placed in series with other pipes: (P>>Q)>>R, (P>>Q)>>(R>>S), etc.

4

(5)

DTU Informatics

Department of Informatics and Mathematical Modelling

Constraints for Piping

• The validity of chaining processes by >> depends on the obvious alphabet constraints:

• A further constraint states that the connected channels are capable of transmitting the same kind of message:

(6)

DTU Informatics

Department of Informatics and Mathematical Modelling

Example

6

(7)

DTU Informatics

Department of Informatics and Mathematical Modelling

Example

• Every number input is doubled before it is output:

αleft(DOUBLE) = αright(DOUBLE) = N (natural numbers)

DOUBLE = left?x ➝ right!(x + x) ➝ DOUBLE

(8)

DTU Informatics

Department of Informatics and Mathematical Modelling

Example

6

• Every number input is doubled before it is output:

αleft(DOUBLE) = αright(DOUBLE) = N (natural numbers)

DOUBLE = left?x ➝ right!(x + x) ➝ DOUBLE

• A pipe which outputs each input value multiplied by four:

αleft(QUADRUPLE) = αright(QUADRUPLE) = N

QUADRUPLE = DOUBLE>>DOUBLE

(9)

DTU Informatics

Department of Informatics and Mathematical Modelling

Laws

(10)

DTU Informatics

Department of Informatics and Mathematical Modelling

Laws (cont.)

8

Referencer

Hent nu ( PDF - 10 Sider - 211.00 KB )

RELATEREDE DOKUMENTER

Aalborg Universitet Energy detection using very large antenna array receivers Oliveras Martínez, Àlex; De Carvalho, Elisabeth; Popovski, Petar; Pedersen, Gert Frølund

While in a conventional ED with a small number of antennas, the amplitude of each channel is needed for non-coherent detection, our solution only requires the average channel energy,

On Mereologies in Computing Science

• we show that there is a class of CSP channel and process structures that correspond to the class of mereologies where mereology parts become CSP processes and connectors

Formal Specification of Distributed Systems:Communicating Sequential Processes (CSP)

• Let αNOISYVM = {coin, choc, clink, clunk, toffee}, where clink is the sound of a coin dropping into the money box of a noisy vending machine, and clunk is the sound made by

Formal Specification of Distributed Systems:Communicating Sequential Processes (CSP)

• Example [PAR protocol with numbered ACK]: Sender always waits for positive ACK for latest transmitted message before using next sequence number. OK to count modulo 2

Formal Specification of Distributed Systems:Communicating Sequential Processes (CSP)

• Let αNOISYVM = {coin, choc, clink, clunk, toffee}, where clink is the sound of a coin dropping into the money box of a noisy vending machine, and clunk is the sound made by

Aalborg Universitet An Explorative Study of Qualities in Interactive Processes with Children and Their Parents in Music Therapy during and after Pediatric Hematopoietic Stem Cell Transplantation

An Explorative Study of Qualities in Interactive Processes with Children and Their Parents in Music Therapy during and after Pediatric Hematopoietic Stem Cell Transplantation..

Aalborg Universitet Effectiveness of Sustainability Incorporation In Engieering Curricula A Framework for Course Design Arsat, Din

In a similar model, Creemers and Scheerens have used an input-process-output approach, rather specific termed as a context-input-process-output based approach in

Pipe System Domain Models

Figure 4 on the facing page shows two wells, to the left, each with one output connector (•), two sinks, to the right, each with one input connector, twenty four pipes, each with