CMU MSE 15-671 Models of Software Systems Fall 1995 CSP 2 Garlan & Wing Homework 11 Due: November 15, 1995 1. Communication: Write a CSP process that represents a two-place buffer that has the behavior that it throws away the oldest piece of buffered data if a new one arrives before the oldest is removed. 2. Non-determinism: Consider the following two processes: P = a ¡ P [] b ¡ P Q = a ¡ Q À b ¡ Q a. What are the trace sets of each of these processes? b. Define a process R that distinguishes between the two processes when it is put in parallel with them. That is, R || P has different behavior from R || Q. 3. Reasoning: Simplify the following expression using CSP axioms to eliminate the parallel operator. P = (a ® b ® P | b ® P) Q = (a ® (b ® Q | c ® Q)) Case A. Assuming that aP = {a,b,c} and aQ = {a,b,c} Case B. Assuming that aP = {a,b} and aQ = {a,b,c} 4. Induction: Prove that the process VMS = coin ® choc ® VMS satisfies the specification: FAIR = (tr ¯ coin) ² (tr ¯ choc + 1) 5. Wright: (for this problem refer to the paper "Formalizing Architectural Connection" handed out in the lecture) a. Using Wright, specify a connector for a client-server interaction that has the following properties: The client must initialize the server using a "start-session" event. The server provides two kinds of services, s1 and s2. Each service request generates a reply: r1 and r2 (respectively). Optionally, instead of generating a reply, the server can signal an error after a request for a service. The client may terminate the session using "end-session", after which no more interactions can take place. This should not happen between a request and a reply, however. b. Write a port of a client that uses only service s1, and in addition terminates the session whenever an error is encountered. c. Write a port of a server that accepts requests for services s1, s2, and s3.