CCSWhat is CCS?Why CCS?CCS vs Net TheorySlide 5AgentActionMedium - EtherMedium – Bounded EtherMedium – BufferMedium – Bounded BufferMedium – Shared MemoryHandshakeAgent ExpressionScopeAbstractionN-cell Buffer (1)N-cell Buffer (2)Buffers with acks (1)Buffer with acks (2)Semaphore (1)Semaphore (2)Slide 23SynchronizationTransitionComposition (1)Composition (2)Internal ActionRestrictionTransition Graph.P = P ?The Basic Language (1)The Basic Language (2)The Basic Language (3)Transition Rules (1)Transition Rules (2)Inference Diagram (1)Inference Diagram (2)Inference Diagram (3)DerivativeDerivative Tree (1)Derivative Tree (2)SortSyntactic Sort (1)Syntactic Sort (2)Value PassingAdvanced Topics in Software Engineering 1CCS Introduction Modeling Communication The Basic LanguageAdvanced Topics in Software Engineering 2What 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 3Why CCS? Offers deep insights about concurrency and communication Helps to distinguish essential differences from accidental ones Provides a mathematic treatment that highlights precise modeling and analysisAdvanced Topics in Software Engineering 4CCS vs Net TheoryNet 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 5CCS Introduction Modeling Communication The Basic LanguageAdvanced Topics in Software Engineering 6AgentA 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 7ActionEach 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 8Medium - Ether The sender may always send a message The receiver may always receive a message, provided that a medium is not empty The order of messages may not be preserved.senderreceiverETHERAdvanced Topics in Software Engineering 9Medium – Bounded Ether The sender may always send a message, provided the medium is not full. The receiver may always receive a message, provided that a medium is not empty The order of messages may not be preserved.senderreceiverBoundedETHERAdvanced Topics in Software Engineering 10Medium – Buffer The sender may always send a message. The receiver may always receive a message, provided that a medium is not empty The order of messages is preserved.senderreceiverBufferAdvanced Topics in Software Engineering 11Medium – Bounded Buffer The sender may always send a message, provided the medium is not full. The receiver may always receive a message, provided the medium is not empty. The order of messages is preserved.senderreceiverBoundedBufferAdvanced Topics in Software Engineering 12Medium – Shared Memory The sender may always write an item to a memory location. The receiver may always read an item from a memory location. Writing and reading may occur in any order.sender receiverAdvanced Topics in Software Engineering 13HandshakeEach 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. senderreceiverAdvanced Topics in Software Engineering 14Agent Expression 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. 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.CinoutC defin(x).out(x).CC’(x) defout(x).CC defin(x).C’(x)Advanced Topics in Software Engineering 15ScopeThe 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 16AbstractionAn 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 17N-cell Buffer (1)CinoutC CC(n)defC ^ C ^ ... ^ CC ^ 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 18N-cell Buffer (2)BufferninoutBuffn()defin(x).Buffn(x)Buffn(s:v)defout(v).Buffn(s) (|s| = n – 1) Buffn(s:v)defin(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 19Buffers with acks (1)Din outackin ackoutdefDin(x).out(x).ackout.ackin.DD 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 20Buffer with acks (2)Din outackinackoutDDD(n)defD ^ D ^ ... ^ DQuestion: What is the capacity of D(n)?Advanced Topics in Software Engineering 21Semaphore (1)Semn(0)defget.Semn(1)Semn(k)defget.Semn(k+1) + put.Semn(k-1)Semn(n)defput.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