Advanced Topics in Software Engineering 1 CCS q Introduction q Modeling Communication q The Basic LanguageAdvanced Topics in Software Engineering 2 What is CCS? CCS is a theory of communicating systems that reveals the essence of concurrency and communication. It can also be considered as a formal notation to model and analyze the behavior of concurrent systems.Advanced Topics in Software Engineering 3 Why CCS? q Offers deep insights about concurrency and communication q Helps to distinguish essential differences from accidental ones q Provides a mathematic treatment that highlights precise modeling and analysisAdvanced Topics in Software Engineering 4 CCS vs Net Theory Net theory is a generalization of the theory of automata that allows for the occurrence of independent actions. CCS is based on the notion of observational equivalence, while net theory is concerned with the causality of the actions.Advanced Topics in Software Engineering 5 CCS q Introduction q Modeling Communication q The Basic LanguageAdvanced Topics in Software Engineering 6 Agent A complex system is often composed of several parts that communicate with each other. Each of the parts has its own identity and is called an agent. The term agent will be used broadly: For one purpose, we take it to be atomic; for other purposes, we take it as a composition of sub-agents.Advanced Topics in Software Engineering 7 Action Each action of an agent is either an interaction with its neighboring agents, and then it is communication, or it occurs independently of them and then it may occur concurrently with their actions. A central idea in CCS is observational equivalence: Two agents are equivalent if they exhibit the same behavior in terms of observable actions.Advanced Topics in Software Engineering 8 Medium - Ether q The sender may always send a message q The receiver may always receive a message, provided that a medium is not empty q The order of messages may not be preserved. sender receiver ETHERAdvanced Topics in Software Engineering 9 Medium – Bounded Ether q The sender may always send a message, provided the medium is not full. q The receiver may always receive a message, provided that a medium is not empty q The order of messages may not be preserved. sender receiver Bounded ETHERAdvanced Topics in Software Engineering 10 Medium – Buffer q The sender may always send a message. q The receiver may always receive a message, provided that a medium is not empty q The order of messages is preserved. sender receiver BufferAdvanced Topics in Software Engineering 11 Medium – Bounded Buffer q The sender may always send a message, provided the medium is not full. q The receiver may always receive a message, provided the medium is not empty. q The order of messages is preserved. sender receiver Bounded BufferAdvanced Topics in Software Engineering 12 Medium – Shared Memory q The sender may always write an item to a memory location. q The receiver may always read an item from a memory location. q Writing and reading may occur in any order. sender receiverAdvanced Topics in Software Engineering 13 Handshake Each arrow in each diagram is a single action, called handshake, that is indivisible in time and consists of the passage of a piece of information between two entities. We consider that medium is no different from sender/receiver, in the sense that they are participants of a handshake. sender receiverAdvanced Topics in Software Engineering 14 Agent Expression q C is an agent that may hold a single data item. It can accept an item at port in, and deliver an item at port out. q in(x) stands for a handshake in which an item is received at in, and out(x) stands for a handshake in which an item is delivered at out. C in out C def in(x).out(x).C Cʼ(x) def out(x).C C def in(x).Cʼ(x)Advanced Topics in Software Engineering 15 Scope The scope of a variable on the left-hand side of a defining equation is the entire equation. The scope of a variable in a prefix on the right-hand side is the agent expression which begins with the prefix. Note that a variable never has scope larger than a single equation.Advanced Topics in Software Engineering 16 Abstraction An agent can be specified at different levels of abstraction – either directly in terms of its interactions with the environment, or indirectly in terms of its composition from smaller agents. One important power provided by CCS is to prove that agents specified at different levels of abstractions are equivalent.Advanced Topics in Software Engineering 17 N-cell Buffer (1) C in out C C C(n) def C ^ C ^ ... ^ C C ^ C represents an agent formed by linking the out port of the first sub-agent C with the in port of the second sub-agent C.Advanced Topics in Software Engineering 18 N-cell Buffer (2) Buffern in out Buffn(ε) def in(x).Buffn(x) Buffn(s:v) def out(v).Buffn(s) (|s| = n – 1) Buffn(s:v) def in(x).Buffn(x : s : v) + out(v).Buffn(s) (|s| < n – 1) • P + Q represents an agent that behaves like P or Q; as soon as one performs its first action, the other is discarded. • ε - empty sequence; : - sequence concatenation.Advanced Topics in Software Engineering 19 Buffers with acks (1) Din out ackin ackout def D in(x).out(x).ackout.ackin.D D will acknowledge the receipt of an input value only after it has delivered the value as output and also received acknowledgement for it.Advanced Topics in Software Engineering 20 Buffer with acks (2) Din out ackin ackout DDD(n) def D ^ D ^ ... ^ D Question: What is the capacity of D(n)?Advanced Topics in Software Engineering 21 Semaphore (1) Semn(0) def get.Semn(1) Semn(k) def get.Semn(k+1) + put.Semn(k-1) Semn(n) def put.Semn(n-1) Note that Semn admits any sequence of gets and puts in which the number of gets minus the number of puts lies in the range of 0 to n inclusive. Question: What is the difference between Semn and Buffn?Advanced Topics in Software Engineering 22 Semaphore (2) Sem(n) def Sem | Sem | ... | Sem Composition (|) : Agent P | Q is a system in which P and Q may proceed independently but may also interact through complementary ports. Sem get put Sem get put Sem get putAdvanced Topics in Software Engineering 23 CCS q Introduction q Modeling Communication q The Basic