the semantics of channel in CSP#

View previous topic View next topic Go down

the semantics of channel in CSP#

Post  alex2ren on Mon Dec 03, 2012 4:48 pm

Q1: It seems to me that the channel is CSP# is totally different from that in CSPm. But in the document 3.1.1.2, it says "One exception is the channel names are allowed, because we may want to use channel name in a specific process to simulate the channel behaviors and use refinement checking to compare with real channel events." Is there any example illustrating this idea? Thanks.

Q2: What's the semantics of P4 in the following model? Is P4 a refinement of P5?

channel ch 0;

P0 = ch!3 -> e -> P0;
P1 = ch?x -> e -> P1;
P2 = ch?x -> e -> P2;


P4 = P0 || P1 || P2;
P5 = ch!3 -> e -> P5;

alex2ren

Posts : 6
Join date : 2012-12-03

View user profile

Back to top Go down

Re: the semantics of channel in CSP#

Post  pat team on Thu Dec 06, 2012 3:27 pm

For Q1: please refer to the following paper for a more detailed discussion.
http://www.comp.nus.edu.sg/~pat/publications/icfem12%20comparison.pdf

in CSP#, channel is more like a Promela channel so that they can be synchronous or asynchronous.
You can use channel name as event name as shown in the following, we don't have restriction on the use of channel name. c becomes a channel if it is used as a channel communication. the event c is an normal event, and has nothing to do with channel c.
channel c 0;
P = a -> c -> Skip;

For Q2: you can use the PAT simulator to draw its graph. then you can see that channel are pair-wise synchronization. for synchronous channel, they will become . after the synchronization.
that is P1 sync with P2 becomes ch.3, which is missing in P5, so the refinement doesn't hold.

Let us know if you have more questions.

alex2ren wrote:Q1: It seems to me that the channel is CSP# is totally different from that in CSPm. But in the document 3.1.1.2, it says "One exception is the channel names are allowed, because we may want to use channel name in a specific process to simulate the channel behaviors and use refinement checking to compare with real channel events." Is there any example illustrating this idea? Thanks.

Q2: What's the semantics of P4 in the following model? Is P4 a refinement of P5?

channel ch 0;

P0 = ch!3 -> e -> P0;
P1 = ch?x -> e -> P1;
P2 = ch?x -> e -> P2;


P4 = P0 || P1 || P2;
P5 = ch!3 -> e -> P5;

pat team
Admin

Posts : 17
Join date : 2010-02-15

View user profile http://www.comp.nus.edu.sg/~pat/

Back to top Go down

View previous topic View next topic Back to top

- Similar topics

 
Permissions in this forum:
You cannot reply to topics in this forum