Main Page: Difference between revisions

From formulasearchengine
Jump to navigation Jump to search
No edit summary
No edit summary
Line 1: Line 1:
{{Infobox scientist
In [[computer science]], '''Communicating Sequential Processes''' ('''CSP''') is a [[specification language|formal language]] for describing [[pattern]]s of [[interaction]] in [[concurrent systems]].<ref name="roscoe">{{cite book|first=A. W.|last=Roscoe|authorlink=Bill Roscoe|title=The Theory and Practice of Concurrency|publisher=[[Prentice Hall]]|isbn = 0-13-674409-5|year=1997}}</ref> It is a member of the family of mathematical theories of concurrency known as process algebras, or [[process calculus|process calculi]], based on [[message passing]] via [[Channel (programming)|channels]]. CSP was highly influential in the design of the [[occam (programming language)|occam]] programming language,<ref name="roscoe"/><ref>{{cite book|last=INMOS|authorlink=INMOS|url=http://www.wotug.org/occam/documentation/oc21refman.pdf|format=PDF|title=occam 2.1 Reference Manual|publisher=SGS-THOMSON Microelectronics Ltd.|date=1995-05-12}}, INMOS document 72 occ 45 03</ref> and also influenced the design of programming languages such as [[Limbo (programming language)|Limbo]]<ref>{{cite web|title=Resources about threaded programming in the Bell Labs CSP style|url=http://swtch.com/~rsc/thread/|accessdate=2010-04-15}}</ref> and [[Go (programming language)|Go]].<ref name="golang">{{cite web |title=Language Design FAQ: Why build concurrency on the ideas of CSP? |url=http://golang.org/doc/go_faq.html#csp}}</ref>
|name = Walter H. Schottky
|image = Walter Hermann Schottky (1886-1976).jpg
|image_size = 200px
|caption =
|birth_date = {{birth-date|23 July 1886|23 July 1886}}
|birth_place = [[Zürich]], [[Switzerland]]
|death_date = {{death-date|4 March 1976|4 March 1976}}
|death_place = [[Pretzfeld]], [[West Germany]]
|residence = Germany
|citizenship =
|nationality = German
|ethnicity =
|fields = [[Physicist]]
|workplaces = [[University of Jena]]<br />[[University of Würzburg]]<br />[[University of Rostock]]<br />[[Siemens AG|Siemens Research Laboratories]]
|alma_mater = [[University of Berlin]]
|doctoral_advisor = [[Max Planck]]<br />[[Heinrich Rubens]]
|academic_advisors =
|doctoral_students =
|notable_students = [[Werner Hartmann (physicist)|Werner Hartmann]]
|known_for = [[Schottky effect]]<br />[[Schottky barrier]]<br />[[Schottky contact]]<br />[[Schottky anomaly]]<br />[[Screen-grid|Screen-grid vacuum tube]]<br />[[Tetrode]]<br />[[Ribbon microphone]]<br />[[Loudspeaker#Ribbon_and_planar_magnetic_loudspeakers|Ribbon loudspeaker]]<br />[[Field electron emission|Theory of Field emission]]<br />[[Shot noise]]
|author_abbrev_bot =
|author_abbrev_zoo =
|influences =
|influenced =
|awards = [[Hughes medal]] (1936)<br />[[Werner von Siemens Ring]] (1964)
|religion =
|signature = <!--(filename only)-->
|footnotes = His father was the [[mathematician]] [[Friedrich Hermann Schottky]].
}}
'''Walter Hermann Schottky''' (23 July 1886, [[Zürich]], Switzerland – 4 March 1976, [[Pretzfeld]], West Germany) was a German physicist who played a major early role in developing the theory of electron and ion emission phenomena, invented the [[Screen-grid#Screen grid|screen-grid]] [[vacuum tube]] in 1915 and the [[pentode]]{{Citation needed|date=March 2011}} in 1919 while working at [[Siemens AG|Siemens]], co-invented the [[Ribbon microphone]] and [[Loudspeaker#Ribbon_and_planar_magnetic_loudspeakers|Ribbon Loudspeaker]] along with Dr. Gerwin Erlach in 1924<ref name="Ribbon">{{Cite news|url=http://www.hi-fiworld.co.uk/loudspeakers/66-knowledge/152-historically-speaking-part-ii.html|title=Historically Speaking|publisher=Hifi World|date=April 2008|accessdate=April 2012}}</ref> and later made many significant contributions in the areas of semiconductor devices, technical physics and technology.


==Education==
CSP was first described in a 1978 paper by [[C. A. R. Hoare]],<ref name="hoare1978">{{cite journal|last=Hoare
He graduated from the [[Steglitz Gymnasium]], Berlin, Germany in 1904. He obtained his BS in [[Physics]], at the [[University of Berlin]] in 1908. He obtained his PhD in Physics at the [[University of Berlin]] in 1912 under [[Max Planck]] and [[Heinrich Rubens]], with a thesis entitled: ''Zur relativtheoretischen Energetik und Dynamik''.
|first=C. A. R.
|authorlink=C. A. R. Hoare
|title=Communicating sequential processes
|journal=[[Communications of the ACM]]
|volume=21
|issue=8
|pages=666&ndash;677
|year=1978
|doi=10.1145/359576.359585}}
</ref> but has since evolved substantially.<ref name="25years">{{cite book|last=Abdallah
|first=Ali E.|author2=Jones, Cliff B.|author3= Sanders, Jeff W.
|title=Communicating Sequential Processes: The First 25 Years
|series=[[LNCS]]
|volume=3525
|publisher=Springer
|year=2005
|url=http://www.springer.com/computer/theoretical+computer+science/foundations+of+computations/book/978-3-540-25813-1}}
</ref> CSP has been practically applied in industry as a tool for [[formal specification|specifying and verifying]] the concurrent aspects of a variety of different systems, such as the T9000 [[Transputer]],<ref name="barrett">
{{cite journal|last=Barrett
|first=G.
|title=Model checking in practice: The T9000 Virtual Channel Processor
|journal=[[IEEE]] Transactions on Software Engineering
|volume=21
|issue=2
|pages=69–78
|year=1995
|doi=10.1109/32.345823}}</ref> as well as a secure ecommerce system.<ref name="hall">{{cite journal|last = Hall
|first=A
|coauthors=R. Chapman
|url=http://www.anthonyhall.org/c_by_c_secure_system.pdf
|format=PDF|title=Correctness by construction: Developing a commercial secure system
|journal=[[IEEE]] Software
|volume=19
|issue=1
|pages=18–25
|year=2002
|doi=10.1109/52.976937}}
</ref> The theory of CSP itself is also still the subject of active research, including work to increase its range of practical applicability (e.g., increasing the scale of the systems that can be tractably analyzed).<ref>
{{Cite journal|author=Creese, S.|title=Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks|version=D. Phil.|publisher=[[Oxford University]]|year=2001}}
</ref>


==Career==
== History ==
His postdoctoral period was spent at [[University of Jena]] (1912–14). He then lectured at the [[University of Würzburg]] (1919–23). He became Professor of Theoretical Physics, [[University of Rostock]] (1923–27). For two periods he worked at the Siemens Research laboratories (1914–19, 1927–58).
The version of CSP presented in Hoare's original 1978 paper was essentially a concurrent programming language rather than a [[process calculus]]. It had a substantially different [[syntax]] than later versions of CSP, did not possess mathematically defined semantics,<ref name="hoare">{{cite book|last=Hoare|first=C. A. R.|authorlink=C. A. R. Hoare|title=Communicating Sequential Processes|publisher=Prentice Hall|isbn=0-13-153289-8|year=1985}}</ref> and was unable to represent [[unbounded nondeterminism]].<ref name="clinger1981">{{Cite journal|author=William Clinger|authorlink=William Clinger (computer scientist)|title=Foundations of Actor Semantics|url=https://dspace.mit.edu/handle/1721.1/6935|publisher=MIT|version=Mathematics Doctoral Dissertation|date=June 1981}}</ref> Programs in the original CSP were written as a parallel composition of a fixed number of sequential processes communicating with each other strictly through synchronous message-passing. In contrast to later versions of CSP, each process was assigned an explicit name, and the source or destination of a message was defined by specifying the name of the intended sending or receiving process. For example the process


==Inventions==
COPY = *[c:character; west?c → east!c]
In 1924, Schottky co-invented the [[Ribbon microphone]] along with Dr. Gerwin Erlach. The idea was that a very fine ribbon suspended in a magnetic field could generate electric signals. This in turn lead also to the invention of the [[Loudspeaker#Ribbon_and_planar_magnetic_loudspeakers|Ribbon Loudspeaker]] by using it in the reverse order, but not until high flux permanent magnets became available in the late 1930s.<ref name="Ribbon"></ref>


==Major scientific achievements==
repeatedly receives a character from the process named <code>west</code>, and then sends that character to process named <code>east</code>. The parallel composition
Possibly, in retrospect, Schottky's most important scientific achievement was to develop (in 1914) the well-known classical formula, now written -''q''<sup>2</sup>/16π''ε''<sub>0</sub>''x'', for the interaction energy between a point [[electric charge|charge]] ''q'' and a ''flat'' metal surface, when the charge is at a distance ''x'' from the surface. Owing to the method of its derivation, this interaction is called the "image potential energy" (image PE). Schottky based his work on earlier work by [[William Thomson, 1st Baron Kelvin|Lord Kelvin]] relating to the image PE for a sphere. Schottky's image PE has become a standard component in simple models of the barrier to motion, ''M''(''x''), experienced by an electron on approaching a metal surface or a metal–[[semiconductor]] interface from the inside. (This ''M''(''x'') is the quantity that appears when the one-dimensional, one-particle, [[Schrödinger equation]] is written in the form


:<math>\frac{d^2}{dx^2} \Psi(x) = \frac{2m}{\hbar^2} M(x) \Psi(x) .</math>
[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]


Here, <math> \hbar </math> is [[Planck's constant]] divided by 2π, and ''m'' is the [[electron mass]].)
assigns the names <code>west</code> to the <code>DISASSEMBLE</code> process, <code>X</code> to the <code>COPY</code> process, and <code>east</code> to the <code>ASSEMBLE</code> process, and executes these three processes concurrently.<ref name="hoare1978"/>


The image PE is usually combined with terms relating to an applied [[electric field]] ''F'' and to the height ''h'' (in the absence of any field) of the barrier. This leads to the following expression for the dependence of the barrier energy on distance ''x'', measured from the "electrical surface" of the metal, into the [[vacuum]] or into the [[semiconductor]]:
Following the publication of the original version of CSP, Hoare, [[Stephen Brookes]], and [[Bill Roscoe|A. W. Roscoe]] developed and refined the ''theory'' of CSP into its modern, process algebraic form. The approach taken in developing CSP into a process algebra was influenced by [[Robin Milner]]'s work on the [[Calculus of Communicating Systems]] (CCS), and vice versa. The theoretical version of CSP was initially presented in a 1984 article by Brookes, Hoare, and Roscoe,<ref>{{cite journal|first=Stephen|last=Brookes|coauthors=[[C. A. R. Hoare]] and [[Bill Roscoe|A. W. Roscoe]]|title=A Theory of Communicating Sequential Processes|journal=[[Journal of the ACM]]|volume=31|issue=3|pages=560&ndash;599|year=1984|doi=10.1145/828.833}}</ref> and later in Hoare's book ''Communicating Sequential Processes'',<ref name="hoare"/> which was published in 1985. In September 2006, that book was still the [http://citeseer.ist.psu.edu/articles.html third-most cited] [[computer science]] reference of all time according to [[Citeseer]] (albeit an unreliable source due to the nature of its sampling). The theory of CSP has undergone a few minor changes since the publication of Hoare's book. Most of these changes were motivated by the advent of automated tools for CSP process analysis and verification. Roscoe's ''The Theory and Practice of Concurrency''<ref name="roscoe"/> describes this newer version of CSP.


:<math> M(x) = \; h -eFx - e^2/4 \pi \epsilon_0 \epsilon_r x \;. </math>
=== Applications ===
An early and important application of CSP was its use for specification and verification of elements of the INMOS T9000 [[Transputer]], a complex superscalar pipelined processor designed to support large-scale multiprocessing. CSP was employed in verifying the correctness of both the processor pipeline, and the Virtual Channel Processor which managed off-chip communications for the processor.<ref name="barrett"/>


Here, ''e'' is the [[elementary charge|elementary positive charge]], ''ε''<sub>0</sub> is the [[electric constant]] and ''ε''<sub>r</sub> is the [[relative permittivity]] of the second medium (=1 for [[vacuum]]). In the case of a [[metal–semiconductor junction]], this is called a [[Schottky barrier]]; in the case of the metal-vacuum interface, this is sometimes called a [[Field electron emission|Schottky–Nordheim barrier]]. In many contexts, ''h'' has to be taken equal to the local [[work function]] ''φ''.
Industrial application of CSP to software design has usually focused on dependable and safety-critical systems. For example, the Bremen Institute for Safe Systems and [[DaimlerChrysler Aerospace|Daimler-Benz Aerospace]] modeled a fault management system and avionics interface (consisting of some 23,000 lines of code) intended for use on the International Space Station in CSP, and analyzed the model to confirm that their design was free of deadlock and livelock.<ref>{{cite conference|first=B. |last=Buth|coauthors=M. Kouvaras, J. Peleska, and H. Shi|title=Deadlock analysis for a fault-tolerant system|booktitle=Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97)| pages = 60–75|date=December 1997}}</ref><ref>{{cite conference|first=B.|last=Buth|coauthors=J. Peleska, and H. Shi|title=Combining methods for the livelock analysis of a fault-tolerant system|booktitle=Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98)|pages=124– 139|date=January 1999}}</ref> The modeling and analysis process was able to uncover a number of errors that would have been difficult to detect using testing alone. Similarly, [[Praxis High Integrity Systems]] applied CSP modeling and analysis during the development of software (approximately 100,000 lines of code) for a secure smart-card Certification Authority to verify that their design was secure and free of deadlock. Praxis claims that the system has a much lower defect rate than comparable systems.<ref name="hall"/>


This [[Field electron emission|Schottky–Nordheim barrier]] (SN barrier) has played in important role in the theories of [[thermionic emission]] and of [[field electron emission]]. Applying the field causes lowering of the barrier, and thus enhances the emission current in [[thermionic emission]]. This is called the "[[Thermionic emission|Schottky effect]]", and the resulting emission regime is called "[[Thermionic emission|Schottky emission]]".
Since CSP is well-suited to modeling and analyzing systems that incorporate complex message exchanges, it has also been applied to the verification of communications and security protocols. A prominent example of this sort of application is Lowe’s use of CSP and the [[FDR2|FDR refinement-checker]] to discover a previously unknown attack on the [[Needham-Schroeder protocol|Needham-Schroeder public-key authentication protocol]], and then to develop a corrected protocol able to defeat the attack.<ref>{{cite conference|first=G. |last=Lowe|title=Breaking and fixing the Needham-Schroeder public-key protocol using FDR|booktitle=Tools and Algorithms for the Construction and Analysis of Systems (TACAS)|pages=147–166.|publisher=Springer-Verlag|year=1996|url=http://citeseer.ist.psu.edu/lowe96breaking.html}}</ref>


In 1923 Schottky suggested (incorrectly) that the experimental phenomenon then called autoelectronic emission and now called [[field electron emission]] resulted when the barrier was pulled down to zero. In fact, the effect is due to [[quantum tunnelling|wave-mechanical tunneling]], as shown by Fowler and Nordheim in 1928. But the [[Field electron emission|SN barrier]] has now become the standard model for the tunneling barrier.
== Informal description ==
As its name suggests, CSP allows the description of systems in terms of component processes that operate independently, and interact with each other solely through [[message passing|message-passing]] communication. However, the ''"Sequential"'' part of the CSP name is now something of a misnomer, since modern CSP allows component processes to be defined both as sequential processes, and as the parallel composition of more primitive processes. The relationships between different processes, and the way each process communicates with its environment, are described using various [[process calculi|process algebraic]] operators. Using this algebraic approach, quite complex process descriptions can be easily constructed from a few primitive elements.


Later, in the context of [[semiconductor devices]], it was suggested that a similar barrier should exist at the junction of a metal and a semiconductor. Such barriers are now widely known as [[Schottky barrier]]s, and considerations apply to the transfer of electrons across them that are analogous to the older considerations of how electrons are emitted from a metal into vacuum. (Basically, several emission regimes exist, for different combinations of field and temperature. The different regimes are governed by different approximate formulae.)
=== Primitives ===
CSP provides two classes of primitives in its process algebra:
;Events
:Events represent communications or interactions. They are assumed to be indivisible and instantaneous.  They may be atomic names (e.g. ''on'', ''off''), compound names (e.g. ''valve.open'', ''valve.close''), or input/output events (e.g. ''mouse?xy'', ''screen!bitmap'').
;Primitive processes:
:Primitive processes represent fundamental behaviors: examples include ''STOP'' (the process that communicates nothing, also called [[deadlock]]), and ''SKIP'' (which represents successful termination).


When the whole behaviour of such interfaces is examined, it is found that they can act (asymmetrically) as a special form of electronic diode, now called a [[Schottky diode]]. In this context, the metal–semiconductor junction is known as a "[[Schottky contact|Schottky (rectifying) contact']]".
=== Algebraic operators ===
CSP has a wide range of algebraic operators. The principal ones are:


Schottky's contributions, in surface science/emission electronics and in semiconductor-device theory, now form a significant and pervasive part of the background to these subjects. It could possibly be argued that – perhaps because they are in the area of technical physics – they are not as generally well recognized as they ought to be.
;Prefix
:The prefix operator combines an event and a process to produce a new process. For example,


==Awards==
::<math>a \rightarrow P</math>
He was awarded the [[Royal Society]]'s [[Hughes medal]] in 1936 for his discovery of the [[Schrot effect]] (spontaneous current variations in high-vacuum discharge tubes, called by him the "Schrot effect": literally, the "small shot effect") in [[thermionic emission]] and his invention of the screen-grid tetrode and a [[superheterodyne]] method of receiving wireless signals.


In 1964 he received the [[Werner von Siemens Ring]] honoring his ground-breaking work on the physical understanding of many phenomena that led to many important technical appliances, among them [[tube amplifier]]s and [[semiconductor]]s.
:is the process which is willing to communicate <math>\mathit{a}</math> with its environment, and, after <math>\mathit{a}</math>, behaves like the process <math>\mathit{P}</math>.


==Controversy==
;Deterministic Choice
The invention of superheterodyne is usually attributed to [[Edwin Armstrong]]. However, Schottky published an article in [[Proc. IRE]] that he had also invented something similar.
:The deterministic (or external) choice operator allows the future evolution of a process to be defined as a choice between two component processes, and allows the environment to resolve the choice by communicating an initial event for one of the processes. For example,
* 1939: first [[p-n junction]]


==Personal life==
::<math>\left(a \rightarrow P\right) \Box \left(b \rightarrow Q\right)</math>
His father was [[mathematician]] [[Friedrich Hermann Schottky]] (1851–1935). His wife was Elizabeth and they had one daughter and two sons. His father was appointed professor of mathematics at the [[University of Zurich]] in 1882, and he was born 4 years later. The family then moved back to Germany in 1892, where his father took up an appointment at the [[University of Marburg]].


==Legacy==
:is the process which is willing to communicate the initial events <math>\mathit{a}</math> and <math>\mathit{b}</math>, and subsequently behaves as either <math>\mathit{P}</math> or <math>\mathit{Q}</math> depending on which initial event the environment chooses to communicate. If both <math>\mathit{a}</math> and <math>\mathit{b}</math> were communicated simultaneously the choice would be resolved nondeterministically.
[[:de:Walter Schottky Institut|Walter Schottky Institute]] (Germany) was named after him. The [[:de:Walter-Schottky-Preis|Walter H. Schottky prize]] is named after him.


==Books written by Schottky==
;Nondeterministic Choice
* ''Thermodynamik'', Julius Springer, Berlin, Germany, 1929.
:The nondeterministic (or internal) choice operator allows the future evolution of a process to be defined as a choice between two component processes, but does not allow the environment any control over which one of the component processes will be selected. For example,
* ''Physik der Glühelektroden'', Akademische Verlagsgesellschaft, Leipzig, 1928.
 
::<math>\left(a \rightarrow P\right) \sqcap \left(b \rightarrow Q\right)</math>
 
:can behave like either <math>\left(a \rightarrow P\right)</math> or <math>\left(b \rightarrow Q\right)</math>. It can refuse to accept <math>\mathit{a}</math> or <math>\mathit{b}</math>, and is only obliged to communicate if the environment offers both <math>\mathit{a}</math> and <math>\mathit{b}</math>. Nondeterminism can be inadvertently introduced into a nominally deterministic choice if the initial events of both sides of the choice are identical. So, for example,
 
::<math>\left(a \rightarrow a \rightarrow STOP\right) \Box \left(a \rightarrow b \rightarrow STOP\right)</math>
 
:is equivalent to
 
::<math>a \rightarrow \left(\left(a \rightarrow STOP\right) \sqcap \left(b \rightarrow STOP\right)\right)</math>
 
;Interleaving
:The interleaving operator represents completely independent concurrent activity. The process
 
::<math>P \;\vert\vert\vert\; Q</math>
 
:behaves as both <math>\mathit{P}</math> and <math>\mathit{Q}</math> simultaneously. The events from both processes are arbitrarily interleaved in time.
 
;Interface Parallel
:The interface parallel operator represents concurrent activity that requires synchronization between the component processes &ndash; any event in the interface set can only occur when ''all'' component processes are able to engage in that event. For example, the process
 
::<math>P \left\vert\left[ \left\{ a \right\} \right]\right\vert Q</math>
 
:requires that <math>\mathit{P}</math> and <math>\mathit{Q}</math> must both be able to perform event <math>\mathit{a}</math> before that event can occur. So, for example, the process
 
::<math>\left(a \rightarrow P\right) \left\vert\left[ \left\{ a \right\} \right]\right\vert \left(a \rightarrow Q\right)</math>
 
:can engage in event <math>\mathit{a}</math>, and become the process
 
::<math>P \left\vert\left[ \left\{ a \right\} \right]\right\vert Q</math>
 
:while
 
::<math>\left (a \rightarrow P\right ) \left\vert\left[ \left\{ a, b \right\} \right]\right\vert \left(b \rightarrow Q\right)</math>
 
:will simply deadlock.
 
;Hiding
:The hiding operator provides a way to abstract processes, by making some events unobservable. A trivial example of hiding is
 
::<math>\left(a \rightarrow P\right) \setminus \left\{ a \right\}</math>
 
:which, assuming that the event <math>\mathit{a}</math> doesn't appear in <math>\mathit{P}</math>, simply reduces to
 
::<math>\mathit{P}</math>
 
=== Examples ===
One of the archetypal CSP examples is an abstract representation of a chocolate vending machine and its interactions with a person wishing to buy some chocolate. This vending machine might be able to carry out two different events, “coin” and “choc” which represent the insertion of payment and the delivery of a chocolate respectively. A machine which demands payment before offering a chocolate can be written as:
 
:<math>\textit{VendingMachine} = \textit{coin} \rightarrow \textit{choc} \rightarrow \textit{STOP}</math>
 
A person who might choose to use a coin or card to make payments could be modelled as:
 
:<math>\textit{Person} = (\textit{coin} \rightarrow \textit{STOP}) \Box (\textit{card} \rightarrow \textit{STOP})</math>
 
These two processes can be put in parallel, so that they can interact with each other. The behaviour of the composite process depends on the events that the two component processes must synchronise on. Thus,
 
:<math>\textit{VendingMachine} \left\vert\left[\left\{ \textit{coin}, \textit{card} \right\}\right]\right\vert \textit{Person} \equiv \textit{coin} \rightarrow \textit{choc} \rightarrow \textit{STOP}</math>
 
whereas if synchronization was only required on “coin”, we would obtain
 
:<math>\textit{VendingMachine} \left\vert\left[\left\{ \textit{coin} \right\}\right]\right\vert \textit{Person} \equiv \left (\textit{coin} \rightarrow \textit{choc} \rightarrow \textit{STOP}\right ) \Box \left (\textit{card} \rightarrow \textit{STOP}\right )</math>
 
If we abstract this latter composite process by hiding the “coin” and “card” events, i.e.
 
:<math>\left (\left (\textit{coin} \rightarrow \textit{choc} \rightarrow \textit{STO}P\right ) \Box \left (\textit{card} \rightarrow \textit{STOP}\right )\right ) \setminus \left\{\textit{coin}, card\right\}</math>
 
we get the nondeterministic process
 
:<math>\left (\textit{choc} \rightarrow \textit{STOP}\right ) \sqcap \textit{STOP}</math>
 
This is a process which either offers a “choc” event and then stops, or just stops. In other words, if we treat the abstraction as an external view of the system (e.g., someone who does not see the decision reached by the person), [[Nondeterministic algorithm|nondeterminism]] has been introduced.
 
== Formal definition ==
=== Syntax ===
The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let <math>\mathit{e}</math> be an event, and <math>\mathit{X}</math> be a set of events. Then the basic [[syntax]] of CSP can be defined as:
 
:<math>
\begin{matrix}
Proc & ::= & \textit{STOP} & \; \\
&|& \textit{SKIP} & \; \\
&|& e \rightarrow \textit{Proc} & (\text{prefixing})\\
&|& \textit{Proc} \;\Box\; \textit{Proc} & (\text{external} \; \text{choice})\\
&|& \textit{Proc} \;\sqcap\; \textit{Proc} & (\text{nondeterministic} \; \text{choice})\\
&|& \textit{Proc} \;\vert\vert\vert\; \textit{Proc} & (\text{interleaving}) \\
&|& \textit{Proc} \;|[ \{ X \} ]| \;\textit{Proc} & (\text{interface} \; \text{parallel})\\
&|& \textit{Proc} \setminus X & (\text{hiding})\\
&|& \textit{Proc} ; \textit{Proc} & (\text{sequential} \; \text{composition})\\
&|& \mathrm{if} \; b \; \mathrm{then} \; \textit{Proc}\; \mathrm{else}\; Proc & (\text{boolean} \; \text{conditional})\\
&|& \textit{Proc} \;\triangleright\; \textit{Proc} & (\text{timeout})\\
&|& \textit{Proc} \;\triangle\; \textit{Proc} & (\text{interrupt})
\end{matrix}
</math>
 
Note that, in the interests of brevity, the syntax presented above omits the <math>\mathbf{div}</math> process, which represents [[Divergence (computer science)|divergence]], as well as various operators such as alphabetized parallel, piping, and indexed choices.
 
=== Formal semantics ===
{{Expand section|date=June 2008}}
 
CSP has been imbued with several different [[Semantics#Computer science|formal semantics]], which define the ''meaning'' of syntactically correct CSP expressions. The theory of CSP includes mutually consistent [[denotational semantics]], [[algebraic semantics (computer science)|algebraic semantics]], and [[operational semantics]].
 
==== Denotational semantics ====
The three major denotational models of CSP are the ''traces'' model, the ''stable failures'' model, and the ''failures/divergences'' model. Semantic mappings from process expressions to each of these three models provide the denotational semantics for CSP.<ref name="roscoe"/>
 
The ''traces model'' defines the meaning of a process expression as the set of sequences of events (traces) that the process can be observed to perform. For example,
 
:* <math>traces\left(STOP\right) = \left\{ \langle\rangle \right\}</math> since <math>STOP</math> performs no events
:* <math>traces\left(a\rightarrow b \rightarrow STOP\right) = \left\{\langle\rangle ,\langle a \rangle, \langle a, b \rangle \right\}</math> since the process <math>(a\rightarrow b \rightarrow STOP)</math> can be observed to have performed no events, the event <math>a</math>, or the sequence of events <math>a</math> followed by <math>b</math>
 
More formally, the meaning of a process <math>P</math> in the traces model is defined as <math>traces\left(P\right) \subseteq \Sigma^{\ast}</math> such that:
# <math>\langle\rangle \in traces\left(P\right)</math> (i.e. <math>traces\left(P\right)</math> contains the empty sequence)
# <math>s_1 \smallfrown s_2 \in traces\left(P\right) \implies s_1 \in traces\left(P\right)</math> (i.e. <math>traces\left(P\right)</math> is prefix-closed)
where <math>\Sigma^{\ast}</math> is the set of all possible finite sequences of events.
 
The ''stable failures model'' extends the traces model with refusal sets, which are sets of events <math>X \subseteq \Sigma</math> that a process can refuse to perform. A ''failure'' is a pair <math>\left(s,X\right)</math>, consisting of a trace <math>s</math>, and a refusal set <math>X</math> which identifies the events that a process may refuse once it has executed the trace <math>s</math>. The observed behavior of a process in the stable failures model is described by the pair <math>\left(traces\left(P\right), failures\left(P\right)\right)</math>. For example,
 
:* <math>failures\left(\left(a \rightarrow STOP\right) \Box \left(b \rightarrow STOP\right)\right) = \left\{\left(\langle\rangle,\emptyset\right), \left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math>
:* <math>failures\left(\left(a \rightarrow STOP\right) \sqcap \left(b \rightarrow STOP\right)\right) = \left\{ \left(\langle\rangle,\left\{a\right\}\right), \left(\langle\rangle,\left\{b\right\}\right),
\left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math>
 
The ''failures/divergence model'' further extends the failures model to handle [[divergence (computer science)|divergence]]. The semantics of a process in the failures/divergences model is a pair <math>\left(failures_\perp\left(P\right), divergences\left(P\right)\right)</math> where <math>divergences\left(P\right)</math> is defined as the set of all traces that can lead to divergent behavior and <math>failures_\perp\left(P\right) = failures\left(P\right) \cup \left\{\left(s,X\right) \vert s \in divergences\left(P\right)\right\}</math>.
 
== Tools ==
 
Over the years, a number of tools for analyzing and understanding systems described using CSP have been produced. Early tool implementations used a variety of machine-readable syntaxes for CSP, making input files written for different tools incompatible. However, most CSP tools have now standardized on the machine-readable dialect of CSP devised by Bryan Scattergood, sometimes referred to as CSP<sub>''M''</sub>.<ref>{{Cite journal|author=Scattergood, J.B.|title=The Semantics and Implementation of Machine-Readable CSP|version=D.Phil.|publisher=[[Oxford University Computing Laboratory]]|year=1998}}</ref> The CSP<sub>''M''</sub> dialect of CSP possesses a formally defined [[operational semantics]], which includes an embedded [[functional programming language]].
 
The most well-known CSP tool is probably ''Failures/Divergence Refinement 2'' (''[[FDR2]]''), which is a commercial product developed by Formal Systems (Europe) Ltd. FDR2 is often described as a [[model checker]], but is technically a ''refinement'' checker, in that it converts two CSP process expressions into [[Labelled transition system|Labelled Transition System]]s (LTSs), and then determines whether one of the processes is a refinement of the other within some specified semantic model (traces, failures, or failures/divergence).<ref>{{Cite journal|author=A.W. Roscoe|title=Model-checking CSP|version=In ''A Classical Mind: essays in Honour of C.A.R. Hoare''|publisher=Prentice Hall|year=1994|authorlink=Bill Roscoe}}</ref> FDR2 applies various state-space compression algorithms to the process LTSs in order to reduce the size of the state-space that must be explored during a refinement check.
 
The ''Adelaide Refinement Checker'' (''ARC'') <ref>{{cite conference |first=Atanas N. |last=  Parashkevov|coauthors=Jay Yantchev  |title=ARC - a tool for efficient refinement and equivalence checking for CSP |booktitle=IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96 |pages= 68–75|year=1996 |url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.3212 |accessdate=2008-11-26 }}</ref> is a CSP refinement checker developed by the Formal Modelling and Verification Group at [[The University of Adelaide]]. ARC differs from FDR2 in that it internally represents CSP processes as [[Binary decision diagram|Ordered Binary Decision Diagram]]s (OBDDs), which alleviates the state explosion problem of explicit LTS representations without requiring the use of state-space compression algorithms such as those used in FDR2.
 
The ''ProB'' project,<ref>{{cite conference| first = Michael |last=Leuschel |coauthors= Marc Fontaine| title = Probing the Depths of CSP-M: A new FDR-compliant Validation Tool| booktitle = ICFEM 2008|publisher = Springer-Verlag|year=2008|url=http://www.stups.uni-duesseldorf.de/publications/main.pdf|format=PDF|accessdate=2008-11-26}}</ref> which is hosted by the Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, was originally created to support analysis of specifications constructed in the [[B method]]. However, it also includes support for analysis of CSP processes both through refinement checking, and [[Linear Temporal Logic|LTL]] model-checking. ProB can also be used to verify properties of combined CSP and B specifications.
 
The ''Process Analysis Toolkit'' (PAT)
<ref>{{cite conference|last=Sun |first=Jun|coauthors= Yang Liu and Jin Song Dong|
  title    = PAT: Towards Flexible Verification under Fairness |
  booktitle = Proceedings of the 20th International Conference on Computer-Aided Verification (CAV 2009)|
  publisher = Springer |
  series = Lecture Notes in Computer Science |
  volume    = 5643 |
  year      = 2009 | url = http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf | accessdate = 2009-06-16}}</ref><ref>{{cite conference|last=Sun |first=Jun|coauthors= Yang Liu and Jin Song Dong|
  title    = Model Checking CSP Revisited: Introducing a Process Analysis Toolkit |
  booktitle = Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008)|
  pages    = 307–322 |
  publisher = Springer |
  series = Communications in Computer and Information Science |
  volume    = 17 |
  year      = 2008 | url = http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf | accessdate = 2009-01-15}}</ref> is a CSP analysis tool developed in the School of Computing at the [[National University of Singapore]]. PAT is able to perform refinement checking, LTL model-checking, and simulation of CSP and Timed CSP processes. The PAT process language extends CSP with support for mutable shared variables, asynchronous message passing, and a variety of fairness and quantitative time related process constructs such as <code>deadline</code> and <code>waituntil</code>. The underlying design principle of the PAT process language is to combine a high-level specification language with procedural programs (e.g. an event in PAT may be a sequential program or even an external C# library call) for greater expressiveness. Mutable shared variables and asynchronous channels provide a convenient [[syntactic sugar]] for well-known process modelling patterns used in standard CSP. The PAT syntax is similar, but not identical, to CSP<sub>''M''</sub>.<ref>{{cite conference |first=Jun |last=  Sun|coauthors=Yang Liu, Jin Song Dong and Chunqing Chen  |title=Integrating Specifications and Programs for System Specification and Verification |booktitle=IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09 |year=2009 |url=http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf |accessdate=2009-04-13 }}</ref> The principal differences between the PAT syntax and standard CSP<sub>''M''</sub> are the use of semicolons to terminate process expressions, the inclusion of syntactic sugar for variables and assignments, and the use of slightly different syntax for internal choice and parallel composition.
 
''CSPsim''<ref>{{cite conference|last=Brooke|first=Phillip|coauthors=Richard Paige|title=Lazy Exploration and Checking of CSP Models with CSPsim|booktitle=Communicating Process Architectures 2007|year=2007}}</ref> is a lazy simulator.  It does not model check CSP, but is useful for exploring very large (potentially infinite) systems.
 
== Related formalisms ==
Several other specification languages and formalisms have been derived from, or inspired by, the classic untimed CSP, including:
* [http://citeseer.comp.nus.edu.sg/61363.html Timed CSP], which incorporates timing information for reasoning about real-time systems
* [http://dx.doi.org/10.1007/BF01178564 Receptive Process Theory], a specialization of CSP that assumes an asynchronous (i.e. [[non-blocking algorithm | nonblocking]]) send operation
* [http://www.wotug.org/paperdb/show_pap.php?f=1&num=394 CSPP]
* [http://www.wotug.org/paperdb/show_pap.php?f=1&num=395 HCSP]
* [[Wright (ADL)|Wright]], an architecture description language
* [http://www.comp.nus.edu.sg/~dongjs/tcoz.html TCOZ], an integration of Timed CSP and [[Object Z]]
* [http://www.cs.york.ac.uk/circus/ Circus], an integration of CSP and [[Z specification language|Z]] based on the [[Unifying Theories of Programming]]
* [http://www.compass-research.eu/approach.html CML] (COMPASS Modelling Language), a combination of [http://www.cs.york.ac.uk/circus/ Circus] and [[VDM specification language|VDM]] developed for the modelling of [[System of systems|Systems of Systems]] (SoS)
* [http://www.cs.swan.ac.uk/~csmarkus/Papers/cspcasl.ps CspCASL], an extension of [[Common Algebraic Specification Language|CASL]] that integrates CSP
* [[Language Of Temporal Ordering Specification|LOTOS]], an international standard<ref>[[Language Of Temporal Ordering Specification|ISO 8807, Language of Temporal Ordering Specification]]</ref> that incorporates features of CSP and [[Calculus of Communicating Systems|CCS]].
 
== Comparison with the Actor Model ==
In as much as it is concerned with concurrent processes that exchange messages, the [[Actor model]] is broadly similar to CSP. However, the two models make some fundamentally different choices with regard to the primitives they provide:
 
* CSP processes are anonymous, while actors have identities.
 
* CSP message-passing fundamentally involves a rendezvous between the processes involved in sending and receiving the message, i.e. the sender cannot transmit a message until the receiver is ready to accept it. In contrast, message-passing in actor systems is fundamentally asynchronous, i.e. message transmission and reception do not have to happen at same time, and senders may transmit messages before receivers are ready to accept them. These approaches may be considered duals of each other, in the sense that rendezvous-based systems can be used to construct buffered communications that behave as asynchronous messaging systems, while asynchronous systems can be used to construct rendezvous-style communications by using a message/acknowledgement protocol to synchronize senders and receivers.
 
* CSP uses explicit channels for message passing, whereas actor systems transmit messages to named destination actors. These approaches may also be considered duals of each other, in the sense that processes receiving through a single channel effectively have an identity corresponding to that channel, while the name-based coupling between actors may be broken by constructing actors that behave as channels.


==See also==
==See also==
* [[Schottky defect]]
* [[Occam programming language|occam]] was the first language implementing a CSP model.
* [[Ease programming language]] combines the process constructs of CSP with logically shared data structures.
* [[JCSP]] is a blending of CSP and [[Occam programming language|occam]] concepts in a [[Java (programming language)|Java]] thread support API.
* [[XC Programming Language|XC]] is a language developed by [[XMOS]] which was heavily influenced by CSP and occam
* [[Limbo (programming language)|Limbo]] is a language that implements concurrency inside the [[Inferno (operating system)|Inferno]] operating system, in a style inspired by CSP.
* [[Plan 9 from Bell Labs]] and [[Plan 9 from User Space]] include the libthread library which allows the use of a CSP-inspired concurrency model from [[C (programming language)|C]].
* [[VerilogCSP]] is a set of [[Macro (computer science)|macros]] added to [[Verilog HDL]] to support Communicating Sequential Processes channel communications.
*[[SystemVerilogCSP]]<ref>{{cite conference|first=A. |last=Saifhashemi|coauthors=P. Beerel|title=SystemVerilogCSP: Modeling Digital Asynchronous Circuits Using SystemVerilog Interfaces|booktitle=Proceedings of Communicating Process Architectures 2011 - WoTUG-
33 (CPA2011)| date=June 2011}}</ref> is a package for [[SystemVerilog]] that enables abstract CSP-like communication actions in [[SystemVerilog]].
* [[Trace monoid]] and [[history monoid]], the mathematical formalism of which CSP is an example.
* [[Trace theory]], the general theory of traces.
* [[Go (programming language)|Go]] is a programming language by [[Google]] incorporating ideas from CSP.<ref name="golang"/><ref>[http://www.youtube.com/watch?v=3DtUzH3zoFo Origins of Go concurrency style]. Talk by Rob Pike at OSCON's Emerging Languages Camp 2010.</ref>
*  [http://clojure.com/blog/2013/06/28/clojure-core-async-channels.html Clojure's Core.async] is a library for the Clojure programming language based on CSP principles.
* [[Joyce (programming language)|Joyce]] is a programming language based on the principles of CSP, developed by [[Brinch Hansen]] around 1989.
* [[SuperPascal]] is a programming language also developed by [[Brinch Hansen]], influenced by CSP and his earlier work with [[Joyce (programming language)|Joyce]].
* [[Ada (programming language)|Ada]] implements features of CSP such as the rendezvous.
* [[Haskell (programming language)|Haskell]] MVars are a rendezvous mechanism for synchronizing threads.<ref>[http://hackage.haskell.org/package/base-4.6.0.1/docs/Control-Concurrent-MVar.html]. Control.Concurrent.MVar </ref>
* [[DirectShow]] is the video framework inside [[DirectX]], it uses the CSP concepts to implement the audio and video filters.
* [[OpenComRTOS]] is a formally developed network-centric distributed [[RTOS]] based on a pragmatic superset of CSP.
 
== Further reading ==
* {{cite book |last=Hoare |first=C. A. R. |authorlink=C. A. R. Hoare |title=Communicating Sequential Processes |origyear=1985 |year=2004 |publisher=Prentice Hall International |format=PDF |url=http://www.usingcsp.com/ |isbn=0-13-153271-5}}
** This book has been updated by [[Jim_Davies_(computer_scientist)|Jim Davies]] at the [[Oxford University Computing Laboratory]] and the new edition is available for download as a PDF file at the [http://www.usingcsp.com/ Using CSP] website.
 
* {{cite book|first=A. W.|last=Roscoe|authorlink=Bill Roscoe|title=The Theory and Practice of Concurrency|publisher=[[Prentice Hall]]|isbn = 0-13-674409-5|year=1997}}
** Some links relating to this book are available [http://web.comlab.ox.ac.uk/oucl/publications/books/concurrency/ here]. The full text is available for download as a [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.ps PS] or [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf PDF] file from Bill Roscoe's [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/pubs.html list] of academic publications.


==References==
==References==
{{Reflist}}
{{reflist|2}}


==External links==
==External links==
* [http://www.tf.uni-kiel.de/matwis/amat/def_en/kap_2/advanced/t2_1_3.html Walter Schottky]
* [http://www.usingcsp.com/ A PDF version of Hoare's CSP book] - Copyright restriction apply, see the page text before downloading.
* [http://www.webcitation.org/query?url=http://www.geocities.com/bioelectrochemistry/schottky.htm&date=2009-10-25+19:12:49 Biography of Walter H. Schottky]
* [http://www.wotug.org/ WoTUG], a User Group for CSP and occam style systems, contains some information about CSP and useful links.
* [http://www.wsi.tum.de/ Walter Schottky Institut]
* [http://citeseerx.ist.psu.edu/search?q=communicating+sequential+processes&submit=Search&sort=rlv&t=doc CSP Citations from CiteSeer]
* {{DNB portal|118759183|TYP=}}
* [https://github.com/loyso/LuaCSP LuaCSP], a framework that allows you to create CSP Occam-like Lua-based programming language embeddable in your application.
* [http://www.gnt-verlag.de/de/?id=88 Reinhard W. Serchinger: Walter Schottky – Atomtheoretiker und Elektrotechniker.] Sein Leben und Werk bis ins Jahr 1941. Diepholz; Stuttgart; Berlin: GNT-Verlag, 2008.
* [http://www.nndb.com/people/438/000172919/ Schottky's nndb profile]
* [http://genealogy.math.ndsu.nodak.edu/id.php?id=55830 Schottky's math genealogy]
 
{{Use dmy dates|date=December 2010}}
 
{{Persondata <!-- Metadata: see [[Wikipedia:Persondata]]. -->
| NAME              = Schottky, Walter H.
| ALTERNATIVE NAMES =
| SHORT DESCRIPTION =
| DATE OF BIRTH    = 23 July 1886
| PLACE OF BIRTH    = [[Zürich]], [[Switzerland]]
| DATE OF DEATH    = 4 March 1976
| PLACE OF DEATH    = [[Pretzfeld]], [[West Germany]]
}}
{{DEFAULTSORT:Schottky, Walter H.}}
[[Category:Semiconductor physicists]]
[[Category:1886 births]]
[[Category:1976 deaths]]
[[Category:German electrical engineers]]
[[Category:German physicists]]
[[Category:Werner von Siemens Ring laureates]]


[[be-x-old:Вальтэр Шоткі]]
{{DEFAULTSORT:Communicating Sequential Processes}}
[[ca:Walter H. Schottky]]
[[Category:1978 introductions]]
[[cs:Walter Schottky]]
[[Category:1978 in computer science]]
[[de:Walter Schottky]]
[[Category:Process calculi]]
[[et:Walter Schottky]]
[[Category:Concurrent computing]]
[[es:Walter H. Schottky]]
[[fr:Walter Schottky]]
[[id:Walter H. Schottky]]
[[it:Walter Schottky]]
[[lt:Walter Schottky]]
[[mr:वॉल्टर शॉट्की]]
[[nl:Walter Schottky]]
[[ja:ヴァルター・ショットキー]]
[[pl:Walter Schottky]]
[[pt:Walter Schottky]]
[[ro:Walter Schottky]]
[[ru:Шоттки, Вальтер]]
[[uk:Вальтер Шотткі]]
[[zh:華特·蕭特基]]

Revision as of 01:32, 11 August 2014

In computer science, Communicating Sequential Processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.[1] It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language,[1][2] and also influenced the design of programming languages such as Limbo[3] and Go.[4]

CSP was first described in a 1978 paper by C. A. R. Hoare,[5] but has since evolved substantially.[6] CSP has been practically applied in industry as a tool for specifying and verifying the concurrent aspects of a variety of different systems, such as the T9000 Transputer,[7] as well as a secure ecommerce system.[8] The theory of CSP itself is also still the subject of active research, including work to increase its range of practical applicability (e.g., increasing the scale of the systems that can be tractably analyzed).[9]

History

The version of CSP presented in Hoare's original 1978 paper was essentially a concurrent programming language rather than a process calculus. It had a substantially different syntax than later versions of CSP, did not possess mathematically defined semantics,[10] and was unable to represent unbounded nondeterminism.[11] Programs in the original CSP were written as a parallel composition of a fixed number of sequential processes communicating with each other strictly through synchronous message-passing. In contrast to later versions of CSP, each process was assigned an explicit name, and the source or destination of a message was defined by specifying the name of the intended sending or receiving process. For example the process

COPY = *[c:character; west?c → east!c]

repeatedly receives a character from the process named west, and then sends that character to process named east. The parallel composition

[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

assigns the names west to the DISASSEMBLE process, X to the COPY process, and east to the ASSEMBLE process, and executes these three processes concurrently.[5]

Following the publication of the original version of CSP, Hoare, Stephen Brookes, and A. W. Roscoe developed and refined the theory of CSP into its modern, process algebraic form. The approach taken in developing CSP into a process algebra was influenced by Robin Milner's work on the Calculus of Communicating Systems (CCS), and vice versa. The theoretical version of CSP was initially presented in a 1984 article by Brookes, Hoare, and Roscoe,[12] and later in Hoare's book Communicating Sequential Processes,[10] which was published in 1985. In September 2006, that book was still the third-most cited computer science reference of all time according to Citeseer (albeit an unreliable source due to the nature of its sampling). The theory of CSP has undergone a few minor changes since the publication of Hoare's book. Most of these changes were motivated by the advent of automated tools for CSP process analysis and verification. Roscoe's The Theory and Practice of Concurrency[1] describes this newer version of CSP.

Applications

An early and important application of CSP was its use for specification and verification of elements of the INMOS T9000 Transputer, a complex superscalar pipelined processor designed to support large-scale multiprocessing. CSP was employed in verifying the correctness of both the processor pipeline, and the Virtual Channel Processor which managed off-chip communications for the processor.[7]

Industrial application of CSP to software design has usually focused on dependable and safety-critical systems. For example, the Bremen Institute for Safe Systems and Daimler-Benz Aerospace modeled a fault management system and avionics interface (consisting of some 23,000 lines of code) intended for use on the International Space Station in CSP, and analyzed the model to confirm that their design was free of deadlock and livelock.[13][14] The modeling and analysis process was able to uncover a number of errors that would have been difficult to detect using testing alone. Similarly, Praxis High Integrity Systems applied CSP modeling and analysis during the development of software (approximately 100,000 lines of code) for a secure smart-card Certification Authority to verify that their design was secure and free of deadlock. Praxis claims that the system has a much lower defect rate than comparable systems.[8]

Since CSP is well-suited to modeling and analyzing systems that incorporate complex message exchanges, it has also been applied to the verification of communications and security protocols. A prominent example of this sort of application is Lowe’s use of CSP and the FDR refinement-checker to discover a previously unknown attack on the Needham-Schroeder public-key authentication protocol, and then to develop a corrected protocol able to defeat the attack.[15]

Informal description

As its name suggests, CSP allows the description of systems in terms of component processes that operate independently, and interact with each other solely through message-passing communication. However, the "Sequential" part of the CSP name is now something of a misnomer, since modern CSP allows component processes to be defined both as sequential processes, and as the parallel composition of more primitive processes. The relationships between different processes, and the way each process communicates with its environment, are described using various process algebraic operators. Using this algebraic approach, quite complex process descriptions can be easily constructed from a few primitive elements.

Primitives

CSP provides two classes of primitives in its process algebra:

Events
Events represent communications or interactions. They are assumed to be indivisible and instantaneous. They may be atomic names (e.g. on, off), compound names (e.g. valve.open, valve.close), or input/output events (e.g. mouse?xy, screen!bitmap).
Primitive processes
Primitive processes represent fundamental behaviors: examples include STOP (the process that communicates nothing, also called deadlock), and SKIP (which represents successful termination).

Algebraic operators

CSP has a wide range of algebraic operators. The principal ones are:

Prefix
The prefix operator combines an event and a process to produce a new process. For example,
is the process which is willing to communicate with its environment, and, after , behaves like the process .
Deterministic Choice
The deterministic (or external) choice operator allows the future evolution of a process to be defined as a choice between two component processes, and allows the environment to resolve the choice by communicating an initial event for one of the processes. For example,
is the process which is willing to communicate the initial events and , and subsequently behaves as either or depending on which initial event the environment chooses to communicate. If both and were communicated simultaneously the choice would be resolved nondeterministically.
Nondeterministic Choice
The nondeterministic (or internal) choice operator allows the future evolution of a process to be defined as a choice between two component processes, but does not allow the environment any control over which one of the component processes will be selected. For example,
can behave like either or . It can refuse to accept or , and is only obliged to communicate if the environment offers both and . Nondeterminism can be inadvertently introduced into a nominally deterministic choice if the initial events of both sides of the choice are identical. So, for example,
is equivalent to
Interleaving
The interleaving operator represents completely independent concurrent activity. The process
behaves as both and simultaneously. The events from both processes are arbitrarily interleaved in time.
Interface Parallel
The interface parallel operator represents concurrent activity that requires synchronization between the component processes – any event in the interface set can only occur when all component processes are able to engage in that event. For example, the process
requires that and must both be able to perform event before that event can occur. So, for example, the process
can engage in event , and become the process
while
will simply deadlock.
Hiding
The hiding operator provides a way to abstract processes, by making some events unobservable. A trivial example of hiding is
which, assuming that the event doesn't appear in , simply reduces to

Examples

One of the archetypal CSP examples is an abstract representation of a chocolate vending machine and its interactions with a person wishing to buy some chocolate. This vending machine might be able to carry out two different events, “coin” and “choc” which represent the insertion of payment and the delivery of a chocolate respectively. A machine which demands payment before offering a chocolate can be written as:

A person who might choose to use a coin or card to make payments could be modelled as:

These two processes can be put in parallel, so that they can interact with each other. The behaviour of the composite process depends on the events that the two component processes must synchronise on. Thus,

whereas if synchronization was only required on “coin”, we would obtain

If we abstract this latter composite process by hiding the “coin” and “card” events, i.e.

we get the nondeterministic process

This is a process which either offers a “choc” event and then stops, or just stops. In other words, if we treat the abstraction as an external view of the system (e.g., someone who does not see the decision reached by the person), nondeterminism has been introduced.

Formal definition

Syntax

The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let be an event, and be a set of events. Then the basic syntax of CSP can be defined as:

Note that, in the interests of brevity, the syntax presented above omits the process, which represents divergence, as well as various operators such as alphabetized parallel, piping, and indexed choices.

Formal semantics

Template:Expand section

CSP has been imbued with several different formal semantics, which define the meaning of syntactically correct CSP expressions. The theory of CSP includes mutually consistent denotational semantics, algebraic semantics, and operational semantics.

Denotational semantics

The three major denotational models of CSP are the traces model, the stable failures model, and the failures/divergences model. Semantic mappings from process expressions to each of these three models provide the denotational semantics for CSP.[1]

The traces model defines the meaning of a process expression as the set of sequences of events (traces) that the process can be observed to perform. For example,

More formally, the meaning of a process in the traces model is defined as such that:

  1. (i.e. contains the empty sequence)
  2. (i.e. is prefix-closed)

where is the set of all possible finite sequences of events.

The stable failures model extends the traces model with refusal sets, which are sets of events that a process can refuse to perform. A failure is a pair , consisting of a trace , and a refusal set which identifies the events that a process may refuse once it has executed the trace . The observed behavior of a process in the stable failures model is described by the pair . For example,

The failures/divergence model further extends the failures model to handle divergence. The semantics of a process in the failures/divergences model is a pair where is defined as the set of all traces that can lead to divergent behavior and .

Tools

Over the years, a number of tools for analyzing and understanding systems described using CSP have been produced. Early tool implementations used a variety of machine-readable syntaxes for CSP, making input files written for different tools incompatible. However, most CSP tools have now standardized on the machine-readable dialect of CSP devised by Bryan Scattergood, sometimes referred to as CSPM.[16] The CSPM dialect of CSP possesses a formally defined operational semantics, which includes an embedded functional programming language.

The most well-known CSP tool is probably Failures/Divergence Refinement 2 (FDR2), which is a commercial product developed by Formal Systems (Europe) Ltd. FDR2 is often described as a model checker, but is technically a refinement checker, in that it converts two CSP process expressions into Labelled Transition Systems (LTSs), and then determines whether one of the processes is a refinement of the other within some specified semantic model (traces, failures, or failures/divergence).[17] FDR2 applies various state-space compression algorithms to the process LTSs in order to reduce the size of the state-space that must be explored during a refinement check.

The Adelaide Refinement Checker (ARC) [18] is a CSP refinement checker developed by the Formal Modelling and Verification Group at The University of Adelaide. ARC differs from FDR2 in that it internally represents CSP processes as Ordered Binary Decision Diagrams (OBDDs), which alleviates the state explosion problem of explicit LTS representations without requiring the use of state-space compression algorithms such as those used in FDR2.

The ProB project,[19] which is hosted by the Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, was originally created to support analysis of specifications constructed in the B method. However, it also includes support for analysis of CSP processes both through refinement checking, and LTL model-checking. ProB can also be used to verify properties of combined CSP and B specifications.

The Process Analysis Toolkit (PAT) [20][21] is a CSP analysis tool developed in the School of Computing at the National University of Singapore. PAT is able to perform refinement checking, LTL model-checking, and simulation of CSP and Timed CSP processes. The PAT process language extends CSP with support for mutable shared variables, asynchronous message passing, and a variety of fairness and quantitative time related process constructs such as deadline and waituntil. The underlying design principle of the PAT process language is to combine a high-level specification language with procedural programs (e.g. an event in PAT may be a sequential program or even an external C# library call) for greater expressiveness. Mutable shared variables and asynchronous channels provide a convenient syntactic sugar for well-known process modelling patterns used in standard CSP. The PAT syntax is similar, but not identical, to CSPM.[22] The principal differences between the PAT syntax and standard CSPM are the use of semicolons to terminate process expressions, the inclusion of syntactic sugar for variables and assignments, and the use of slightly different syntax for internal choice and parallel composition.

CSPsim[23] is a lazy simulator. It does not model check CSP, but is useful for exploring very large (potentially infinite) systems.

Related formalisms

Several other specification languages and formalisms have been derived from, or inspired by, the classic untimed CSP, including:

Comparison with the Actor Model

In as much as it is concerned with concurrent processes that exchange messages, the Actor model is broadly similar to CSP. However, the two models make some fundamentally different choices with regard to the primitives they provide:

  • CSP processes are anonymous, while actors have identities.
  • CSP message-passing fundamentally involves a rendezvous between the processes involved in sending and receiving the message, i.e. the sender cannot transmit a message until the receiver is ready to accept it. In contrast, message-passing in actor systems is fundamentally asynchronous, i.e. message transmission and reception do not have to happen at same time, and senders may transmit messages before receivers are ready to accept them. These approaches may be considered duals of each other, in the sense that rendezvous-based systems can be used to construct buffered communications that behave as asynchronous messaging systems, while asynchronous systems can be used to construct rendezvous-style communications by using a message/acknowledgement protocol to synchronize senders and receivers.
  • CSP uses explicit channels for message passing, whereas actor systems transmit messages to named destination actors. These approaches may also be considered duals of each other, in the sense that processes receiving through a single channel effectively have an identity corresponding to that channel, while the name-based coupling between actors may be broken by constructing actors that behave as channels.

See also

Further reading

  • 20 year-old Real Estate Agent Rusty from Saint-Paul, has hobbies and interests which includes monopoly, property developers in singapore and poker. Will soon undertake a contiki trip that may include going to the Lower Valley of the Omo.

    My blog: http://www.primaboinca.com/view_profile.php?userid=5889534
    • Some links relating to this book are available here. The full text is available for download as a PS or PDF file from Bill Roscoe's list of academic publications.

References

43 year old Petroleum Engineer Harry from Deep River, usually spends time with hobbies and interests like renting movies, property developers in singapore new condominium and vehicle racing. Constantly enjoys going to destinations like Camino Real de Tierra Adentro.

External links

  • A PDF version of Hoare's CSP book - Copyright restriction apply, see the page text before downloading.
  • WoTUG, a User Group for CSP and occam style systems, contains some information about CSP and useful links.
  • CSP Citations from CiteSeer
  • LuaCSP, a framework that allows you to create CSP Occam-like Lua-based programming language embeddable in your application.
  1. 1.0 1.1 1.2 1.3 20 year-old Real Estate Agent Rusty from Saint-Paul, has hobbies and interests which includes monopoly, property developers in singapore and poker. Will soon undertake a contiki trip that may include going to the Lower Valley of the Omo.

    My blog: http://www.primaboinca.com/view_profile.php?userid=5889534
  2. 20 year-old Real Estate Agent Rusty from Saint-Paul, has hobbies and interests which includes monopoly, property developers in singapore and poker. Will soon undertake a contiki trip that may include going to the Lower Valley of the Omo.

    My blog: http://www.primaboinca.com/view_profile.php?userid=5889534, INMOS document 72 occ 45 03
  3. Template:Cite web
  4. 4.0 4.1 Template:Cite web
  5. 5.0 5.1 One of the biggest reasons investing in a Singapore new launch is an effective things is as a result of it is doable to be lent massive quantities of money at very low interest rates that you should utilize to purchase it. Then, if property values continue to go up, then you'll get a really high return on funding (ROI). Simply make sure you purchase one of the higher properties, reminiscent of the ones at Fernvale the Riverbank or any Singapore landed property Get Earnings by means of Renting

    In its statement, the singapore property listing - website link, government claimed that the majority citizens buying their first residence won't be hurt by the new measures. Some concessions can even be prolonged to chose teams of consumers, similar to married couples with a minimum of one Singaporean partner who are purchasing their second property so long as they intend to promote their first residential property. Lower the LTV limit on housing loans granted by monetary establishments regulated by MAS from 70% to 60% for property purchasers who are individuals with a number of outstanding housing loans on the time of the brand new housing purchase. Singapore Property Measures - 30 August 2010 The most popular seek for the number of bedrooms in Singapore is 4, followed by 2 and three. Lush Acres EC @ Sengkang

    Discover out more about real estate funding in the area, together with info on international funding incentives and property possession. Many Singaporeans have been investing in property across the causeway in recent years, attracted by comparatively low prices. However, those who need to exit their investments quickly are likely to face significant challenges when trying to sell their property – and could finally be stuck with a property they can't sell. Career improvement programmes, in-house valuation, auctions and administrative help, venture advertising and marketing, skilled talks and traisning are continuously planned for the sales associates to help them obtain better outcomes for his or her shoppers while at Knight Frank Singapore. No change Present Rules

    Extending the tax exemption would help. The exemption, which may be as a lot as $2 million per family, covers individuals who negotiate a principal reduction on their existing mortgage, sell their house short (i.e., for lower than the excellent loans), or take part in a foreclosure course of. An extension of theexemption would seem like a common-sense means to assist stabilize the housing market, but the political turmoil around the fiscal-cliff negotiations means widespread sense could not win out. Home Minority Chief Nancy Pelosi (D-Calif.) believes that the mortgage relief provision will be on the table during the grand-cut price talks, in response to communications director Nadeam Elshami. Buying or promoting of blue mild bulbs is unlawful.

    A vendor's stamp duty has been launched on industrial property for the primary time, at rates ranging from 5 per cent to 15 per cent. The Authorities might be trying to reassure the market that they aren't in opposition to foreigners and PRs investing in Singapore's property market. They imposed these measures because of extenuating components available in the market." The sale of new dual-key EC models will even be restricted to multi-generational households only. The models have two separate entrances, permitting grandparents, for example, to dwell separately. The vendor's stamp obligation takes effect right this moment and applies to industrial property and plots which might be offered inside three years of the date of buy. JLL named Best Performing Property Brand for second year running

    The data offered is for normal info purposes only and isn't supposed to be personalised investment or monetary advice. Motley Fool Singapore contributor Stanley Lim would not personal shares in any corporations talked about. Singapore private home costs increased by 1.eight% within the fourth quarter of 2012, up from 0.6% within the earlier quarter. Resale prices of government-built HDB residences which are usually bought by Singaporeans, elevated by 2.5%, quarter on quarter, the quickest acquire in five quarters. And industrial property, prices are actually double the levels of three years ago. No withholding tax in the event you sell your property. All your local information regarding vital HDB policies, condominium launches, land growth, commercial property and more

    There are various methods to go about discovering the precise property. Some local newspapers (together with the Straits Instances ) have categorised property sections and many local property brokers have websites. Now there are some specifics to consider when buying a 'new launch' rental. Intended use of the unit Every sale begins with 10 p.c low cost for finish of season sale; changes to 20 % discount storewide; follows by additional reduction of fiftyand ends with last discount of 70 % or extra. Typically there is even a warehouse sale or transferring out sale with huge mark-down of costs for stock clearance. Deborah Regulation from Expat Realtor shares her property market update, plus prime rental residences and houses at the moment available to lease Esparina EC @ Sengkang
  6. 20 year-old Real Estate Agent Rusty from Saint-Paul, has hobbies and interests which includes monopoly, property developers in singapore and poker. Will soon undertake a contiki trip that may include going to the Lower Valley of the Omo.

    My blog: http://www.primaboinca.com/view_profile.php?userid=5889534
  7. 7.0 7.1 One of the biggest reasons investing in a Singapore new launch is an effective things is as a result of it is doable to be lent massive quantities of money at very low interest rates that you should utilize to purchase it. Then, if property values continue to go up, then you'll get a really high return on funding (ROI). Simply make sure you purchase one of the higher properties, reminiscent of the ones at Fernvale the Riverbank or any Singapore landed property Get Earnings by means of Renting

    In its statement, the singapore property listing - website link, government claimed that the majority citizens buying their first residence won't be hurt by the new measures. Some concessions can even be prolonged to chose teams of consumers, similar to married couples with a minimum of one Singaporean partner who are purchasing their second property so long as they intend to promote their first residential property. Lower the LTV limit on housing loans granted by monetary establishments regulated by MAS from 70% to 60% for property purchasers who are individuals with a number of outstanding housing loans on the time of the brand new housing purchase. Singapore Property Measures - 30 August 2010 The most popular seek for the number of bedrooms in Singapore is 4, followed by 2 and three. Lush Acres EC @ Sengkang

    Discover out more about real estate funding in the area, together with info on international funding incentives and property possession. Many Singaporeans have been investing in property across the causeway in recent years, attracted by comparatively low prices. However, those who need to exit their investments quickly are likely to face significant challenges when trying to sell their property – and could finally be stuck with a property they can't sell. Career improvement programmes, in-house valuation, auctions and administrative help, venture advertising and marketing, skilled talks and traisning are continuously planned for the sales associates to help them obtain better outcomes for his or her shoppers while at Knight Frank Singapore. No change Present Rules

    Extending the tax exemption would help. The exemption, which may be as a lot as $2 million per family, covers individuals who negotiate a principal reduction on their existing mortgage, sell their house short (i.e., for lower than the excellent loans), or take part in a foreclosure course of. An extension of theexemption would seem like a common-sense means to assist stabilize the housing market, but the political turmoil around the fiscal-cliff negotiations means widespread sense could not win out. Home Minority Chief Nancy Pelosi (D-Calif.) believes that the mortgage relief provision will be on the table during the grand-cut price talks, in response to communications director Nadeam Elshami. Buying or promoting of blue mild bulbs is unlawful.

    A vendor's stamp duty has been launched on industrial property for the primary time, at rates ranging from 5 per cent to 15 per cent. The Authorities might be trying to reassure the market that they aren't in opposition to foreigners and PRs investing in Singapore's property market. They imposed these measures because of extenuating components available in the market." The sale of new dual-key EC models will even be restricted to multi-generational households only. The models have two separate entrances, permitting grandparents, for example, to dwell separately. The vendor's stamp obligation takes effect right this moment and applies to industrial property and plots which might be offered inside three years of the date of buy. JLL named Best Performing Property Brand for second year running

    The data offered is for normal info purposes only and isn't supposed to be personalised investment or monetary advice. Motley Fool Singapore contributor Stanley Lim would not personal shares in any corporations talked about. Singapore private home costs increased by 1.eight% within the fourth quarter of 2012, up from 0.6% within the earlier quarter. Resale prices of government-built HDB residences which are usually bought by Singaporeans, elevated by 2.5%, quarter on quarter, the quickest acquire in five quarters. And industrial property, prices are actually double the levels of three years ago. No withholding tax in the event you sell your property. All your local information regarding vital HDB policies, condominium launches, land growth, commercial property and more

    There are various methods to go about discovering the precise property. Some local newspapers (together with the Straits Instances ) have categorised property sections and many local property brokers have websites. Now there are some specifics to consider when buying a 'new launch' rental. Intended use of the unit Every sale begins with 10 p.c low cost for finish of season sale; changes to 20 % discount storewide; follows by additional reduction of fiftyand ends with last discount of 70 % or extra. Typically there is even a warehouse sale or transferring out sale with huge mark-down of costs for stock clearance. Deborah Regulation from Expat Realtor shares her property market update, plus prime rental residences and houses at the moment available to lease Esparina EC @ Sengkang
  8. 8.0 8.1 One of the biggest reasons investing in a Singapore new launch is an effective things is as a result of it is doable to be lent massive quantities of money at very low interest rates that you should utilize to purchase it. Then, if property values continue to go up, then you'll get a really high return on funding (ROI). Simply make sure you purchase one of the higher properties, reminiscent of the ones at Fernvale the Riverbank or any Singapore landed property Get Earnings by means of Renting

    In its statement, the singapore property listing - website link, government claimed that the majority citizens buying their first residence won't be hurt by the new measures. Some concessions can even be prolonged to chose teams of consumers, similar to married couples with a minimum of one Singaporean partner who are purchasing their second property so long as they intend to promote their first residential property. Lower the LTV limit on housing loans granted by monetary establishments regulated by MAS from 70% to 60% for property purchasers who are individuals with a number of outstanding housing loans on the time of the brand new housing purchase. Singapore Property Measures - 30 August 2010 The most popular seek for the number of bedrooms in Singapore is 4, followed by 2 and three. Lush Acres EC @ Sengkang

    Discover out more about real estate funding in the area, together with info on international funding incentives and property possession. Many Singaporeans have been investing in property across the causeway in recent years, attracted by comparatively low prices. However, those who need to exit their investments quickly are likely to face significant challenges when trying to sell their property – and could finally be stuck with a property they can't sell. Career improvement programmes, in-house valuation, auctions and administrative help, venture advertising and marketing, skilled talks and traisning are continuously planned for the sales associates to help them obtain better outcomes for his or her shoppers while at Knight Frank Singapore. No change Present Rules

    Extending the tax exemption would help. The exemption, which may be as a lot as $2 million per family, covers individuals who negotiate a principal reduction on their existing mortgage, sell their house short (i.e., for lower than the excellent loans), or take part in a foreclosure course of. An extension of theexemption would seem like a common-sense means to assist stabilize the housing market, but the political turmoil around the fiscal-cliff negotiations means widespread sense could not win out. Home Minority Chief Nancy Pelosi (D-Calif.) believes that the mortgage relief provision will be on the table during the grand-cut price talks, in response to communications director Nadeam Elshami. Buying or promoting of blue mild bulbs is unlawful.

    A vendor's stamp duty has been launched on industrial property for the primary time, at rates ranging from 5 per cent to 15 per cent. The Authorities might be trying to reassure the market that they aren't in opposition to foreigners and PRs investing in Singapore's property market. They imposed these measures because of extenuating components available in the market." The sale of new dual-key EC models will even be restricted to multi-generational households only. The models have two separate entrances, permitting grandparents, for example, to dwell separately. The vendor's stamp obligation takes effect right this moment and applies to industrial property and plots which might be offered inside three years of the date of buy. JLL named Best Performing Property Brand for second year running

    The data offered is for normal info purposes only and isn't supposed to be personalised investment or monetary advice. Motley Fool Singapore contributor Stanley Lim would not personal shares in any corporations talked about. Singapore private home costs increased by 1.eight% within the fourth quarter of 2012, up from 0.6% within the earlier quarter. Resale prices of government-built HDB residences which are usually bought by Singaporeans, elevated by 2.5%, quarter on quarter, the quickest acquire in five quarters. And industrial property, prices are actually double the levels of three years ago. No withholding tax in the event you sell your property. All your local information regarding vital HDB policies, condominium launches, land growth, commercial property and more

    There are various methods to go about discovering the precise property. Some local newspapers (together with the Straits Instances ) have categorised property sections and many local property brokers have websites. Now there are some specifics to consider when buying a 'new launch' rental. Intended use of the unit Every sale begins with 10 p.c low cost for finish of season sale; changes to 20 % discount storewide; follows by additional reduction of fiftyand ends with last discount of 70 % or extra. Typically there is even a warehouse sale or transferring out sale with huge mark-down of costs for stock clearance. Deborah Regulation from Expat Realtor shares her property market update, plus prime rental residences and houses at the moment available to lease Esparina EC @ Sengkang
  9. One of the biggest reasons investing in a Singapore new launch is an effective things is as a result of it is doable to be lent massive quantities of money at very low interest rates that you should utilize to purchase it. Then, if property values continue to go up, then you'll get a really high return on funding (ROI). Simply make sure you purchase one of the higher properties, reminiscent of the ones at Fernvale the Riverbank or any Singapore landed property Get Earnings by means of Renting

    In its statement, the singapore property listing - website link, government claimed that the majority citizens buying their first residence won't be hurt by the new measures. Some concessions can even be prolonged to chose teams of consumers, similar to married couples with a minimum of one Singaporean partner who are purchasing their second property so long as they intend to promote their first residential property. Lower the LTV limit on housing loans granted by monetary establishments regulated by MAS from 70% to 60% for property purchasers who are individuals with a number of outstanding housing loans on the time of the brand new housing purchase. Singapore Property Measures - 30 August 2010 The most popular seek for the number of bedrooms in Singapore is 4, followed by 2 and three. Lush Acres EC @ Sengkang

    Discover out more about real estate funding in the area, together with info on international funding incentives and property possession. Many Singaporeans have been investing in property across the causeway in recent years, attracted by comparatively low prices. However, those who need to exit their investments quickly are likely to face significant challenges when trying to sell their property – and could finally be stuck with a property they can't sell. Career improvement programmes, in-house valuation, auctions and administrative help, venture advertising and marketing, skilled talks and traisning are continuously planned for the sales associates to help them obtain better outcomes for his or her shoppers while at Knight Frank Singapore. No change Present Rules

    Extending the tax exemption would help. The exemption, which may be as a lot as $2 million per family, covers individuals who negotiate a principal reduction on their existing mortgage, sell their house short (i.e., for lower than the excellent loans), or take part in a foreclosure course of. An extension of theexemption would seem like a common-sense means to assist stabilize the housing market, but the political turmoil around the fiscal-cliff negotiations means widespread sense could not win out. Home Minority Chief Nancy Pelosi (D-Calif.) believes that the mortgage relief provision will be on the table during the grand-cut price talks, in response to communications director Nadeam Elshami. Buying or promoting of blue mild bulbs is unlawful.

    A vendor's stamp duty has been launched on industrial property for the primary time, at rates ranging from 5 per cent to 15 per cent. The Authorities might be trying to reassure the market that they aren't in opposition to foreigners and PRs investing in Singapore's property market. They imposed these measures because of extenuating components available in the market." The sale of new dual-key EC models will even be restricted to multi-generational households only. The models have two separate entrances, permitting grandparents, for example, to dwell separately. The vendor's stamp obligation takes effect right this moment and applies to industrial property and plots which might be offered inside three years of the date of buy. JLL named Best Performing Property Brand for second year running

    The data offered is for normal info purposes only and isn't supposed to be personalised investment or monetary advice. Motley Fool Singapore contributor Stanley Lim would not personal shares in any corporations talked about. Singapore private home costs increased by 1.eight% within the fourth quarter of 2012, up from 0.6% within the earlier quarter. Resale prices of government-built HDB residences which are usually bought by Singaporeans, elevated by 2.5%, quarter on quarter, the quickest acquire in five quarters. And industrial property, prices are actually double the levels of three years ago. No withholding tax in the event you sell your property. All your local information regarding vital HDB policies, condominium launches, land growth, commercial property and more

    There are various methods to go about discovering the precise property. Some local newspapers (together with the Straits Instances ) have categorised property sections and many local property brokers have websites. Now there are some specifics to consider when buying a 'new launch' rental. Intended use of the unit Every sale begins with 10 p.c low cost for finish of season sale; changes to 20 % discount storewide; follows by additional reduction of fiftyand ends with last discount of 70 % or extra. Typically there is even a warehouse sale or transferring out sale with huge mark-down of costs for stock clearance. Deborah Regulation from Expat Realtor shares her property market update, plus prime rental residences and houses at the moment available to lease Esparina EC @ Sengkang
  10. 10.0 10.1 20 year-old Real Estate Agent Rusty from Saint-Paul, has hobbies and interests which includes monopoly, property developers in singapore and poker. Will soon undertake a contiki trip that may include going to the Lower Valley of the Omo.

    My blog: http://www.primaboinca.com/view_profile.php?userid=5889534
  11. One of the biggest reasons investing in a Singapore new launch is an effective things is as a result of it is doable to be lent massive quantities of money at very low interest rates that you should utilize to purchase it. Then, if property values continue to go up, then you'll get a really high return on funding (ROI). Simply make sure you purchase one of the higher properties, reminiscent of the ones at Fernvale the Riverbank or any Singapore landed property Get Earnings by means of Renting

    In its statement, the singapore property listing - website link, government claimed that the majority citizens buying their first residence won't be hurt by the new measures. Some concessions can even be prolonged to chose teams of consumers, similar to married couples with a minimum of one Singaporean partner who are purchasing their second property so long as they intend to promote their first residential property. Lower the LTV limit on housing loans granted by monetary establishments regulated by MAS from 70% to 60% for property purchasers who are individuals with a number of outstanding housing loans on the time of the brand new housing purchase. Singapore Property Measures - 30 August 2010 The most popular seek for the number of bedrooms in Singapore is 4, followed by 2 and three. Lush Acres EC @ Sengkang

    Discover out more about real estate funding in the area, together with info on international funding incentives and property possession. Many Singaporeans have been investing in property across the causeway in recent years, attracted by comparatively low prices. However, those who need to exit their investments quickly are likely to face significant challenges when trying to sell their property – and could finally be stuck with a property they can't sell. Career improvement programmes, in-house valuation, auctions and administrative help, venture advertising and marketing, skilled talks and traisning are continuously planned for the sales associates to help them obtain better outcomes for his or her shoppers while at Knight Frank Singapore. No change Present Rules

    Extending the tax exemption would help. The exemption, which may be as a lot as $2 million per family, covers individuals who negotiate a principal reduction on their existing mortgage, sell their house short (i.e., for lower than the excellent loans), or take part in a foreclosure course of. An extension of theexemption would seem like a common-sense means to assist stabilize the housing market, but the political turmoil around the fiscal-cliff negotiations means widespread sense could not win out. Home Minority Chief Nancy Pelosi (D-Calif.) believes that the mortgage relief provision will be on the table during the grand-cut price talks, in response to communications director Nadeam Elshami. Buying or promoting of blue mild bulbs is unlawful.

    A vendor's stamp duty has been launched on industrial property for the primary time, at rates ranging from 5 per cent to 15 per cent. The Authorities might be trying to reassure the market that they aren't in opposition to foreigners and PRs investing in Singapore's property market. They imposed these measures because of extenuating components available in the market." The sale of new dual-key EC models will even be restricted to multi-generational households only. The models have two separate entrances, permitting grandparents, for example, to dwell separately. The vendor's stamp obligation takes effect right this moment and applies to industrial property and plots which might be offered inside three years of the date of buy. JLL named Best Performing Property Brand for second year running

    The data offered is for normal info purposes only and isn't supposed to be personalised investment or monetary advice. Motley Fool Singapore contributor Stanley Lim would not personal shares in any corporations talked about. Singapore private home costs increased by 1.eight% within the fourth quarter of 2012, up from 0.6% within the earlier quarter. Resale prices of government-built HDB residences which are usually bought by Singaporeans, elevated by 2.5%, quarter on quarter, the quickest acquire in five quarters. And industrial property, prices are actually double the levels of three years ago. No withholding tax in the event you sell your property. All your local information regarding vital HDB policies, condominium launches, land growth, commercial property and more

    There are various methods to go about discovering the precise property. Some local newspapers (together with the Straits Instances ) have categorised property sections and many local property brokers have websites. Now there are some specifics to consider when buying a 'new launch' rental. Intended use of the unit Every sale begins with 10 p.c low cost for finish of season sale; changes to 20 % discount storewide; follows by additional reduction of fiftyand ends with last discount of 70 % or extra. Typically there is even a warehouse sale or transferring out sale with huge mark-down of costs for stock clearance. Deborah Regulation from Expat Realtor shares her property market update, plus prime rental residences and houses at the moment available to lease Esparina EC @ Sengkang
  12. One of the biggest reasons investing in a Singapore new launch is an effective things is as a result of it is doable to be lent massive quantities of money at very low interest rates that you should utilize to purchase it. Then, if property values continue to go up, then you'll get a really high return on funding (ROI). Simply make sure you purchase one of the higher properties, reminiscent of the ones at Fernvale the Riverbank or any Singapore landed property Get Earnings by means of Renting

    In its statement, the singapore property listing - website link, government claimed that the majority citizens buying their first residence won't be hurt by the new measures. Some concessions can even be prolonged to chose teams of consumers, similar to married couples with a minimum of one Singaporean partner who are purchasing their second property so long as they intend to promote their first residential property. Lower the LTV limit on housing loans granted by monetary establishments regulated by MAS from 70% to 60% for property purchasers who are individuals with a number of outstanding housing loans on the time of the brand new housing purchase. Singapore Property Measures - 30 August 2010 The most popular seek for the number of bedrooms in Singapore is 4, followed by 2 and three. Lush Acres EC @ Sengkang

    Discover out more about real estate funding in the area, together with info on international funding incentives and property possession. Many Singaporeans have been investing in property across the causeway in recent years, attracted by comparatively low prices. However, those who need to exit their investments quickly are likely to face significant challenges when trying to sell their property – and could finally be stuck with a property they can't sell. Career improvement programmes, in-house valuation, auctions and administrative help, venture advertising and marketing, skilled talks and traisning are continuously planned for the sales associates to help them obtain better outcomes for his or her shoppers while at Knight Frank Singapore. No change Present Rules

    Extending the tax exemption would help. The exemption, which may be as a lot as $2 million per family, covers individuals who negotiate a principal reduction on their existing mortgage, sell their house short (i.e., for lower than the excellent loans), or take part in a foreclosure course of. An extension of theexemption would seem like a common-sense means to assist stabilize the housing market, but the political turmoil around the fiscal-cliff negotiations means widespread sense could not win out. Home Minority Chief Nancy Pelosi (D-Calif.) believes that the mortgage relief provision will be on the table during the grand-cut price talks, in response to communications director Nadeam Elshami. Buying or promoting of blue mild bulbs is unlawful.

    A vendor's stamp duty has been launched on industrial property for the primary time, at rates ranging from 5 per cent to 15 per cent. The Authorities might be trying to reassure the market that they aren't in opposition to foreigners and PRs investing in Singapore's property market. They imposed these measures because of extenuating components available in the market." The sale of new dual-key EC models will even be restricted to multi-generational households only. The models have two separate entrances, permitting grandparents, for example, to dwell separately. The vendor's stamp obligation takes effect right this moment and applies to industrial property and plots which might be offered inside three years of the date of buy. JLL named Best Performing Property Brand for second year running

    The data offered is for normal info purposes only and isn't supposed to be personalised investment or monetary advice. Motley Fool Singapore contributor Stanley Lim would not personal shares in any corporations talked about. Singapore private home costs increased by 1.eight% within the fourth quarter of 2012, up from 0.6% within the earlier quarter. Resale prices of government-built HDB residences which are usually bought by Singaporeans, elevated by 2.5%, quarter on quarter, the quickest acquire in five quarters. And industrial property, prices are actually double the levels of three years ago. No withholding tax in the event you sell your property. All your local information regarding vital HDB policies, condominium launches, land growth, commercial property and more

    There are various methods to go about discovering the precise property. Some local newspapers (together with the Straits Instances ) have categorised property sections and many local property brokers have websites. Now there are some specifics to consider when buying a 'new launch' rental. Intended use of the unit Every sale begins with 10 p.c low cost for finish of season sale; changes to 20 % discount storewide; follows by additional reduction of fiftyand ends with last discount of 70 % or extra. Typically there is even a warehouse sale or transferring out sale with huge mark-down of costs for stock clearance. Deborah Regulation from Expat Realtor shares her property market update, plus prime rental residences and houses at the moment available to lease Esparina EC @ Sengkang
  13. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  14. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  15. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  16. One of the biggest reasons investing in a Singapore new launch is an effective things is as a result of it is doable to be lent massive quantities of money at very low interest rates that you should utilize to purchase it. Then, if property values continue to go up, then you'll get a really high return on funding (ROI). Simply make sure you purchase one of the higher properties, reminiscent of the ones at Fernvale the Riverbank or any Singapore landed property Get Earnings by means of Renting

    In its statement, the singapore property listing - website link, government claimed that the majority citizens buying their first residence won't be hurt by the new measures. Some concessions can even be prolonged to chose teams of consumers, similar to married couples with a minimum of one Singaporean partner who are purchasing their second property so long as they intend to promote their first residential property. Lower the LTV limit on housing loans granted by monetary establishments regulated by MAS from 70% to 60% for property purchasers who are individuals with a number of outstanding housing loans on the time of the brand new housing purchase. Singapore Property Measures - 30 August 2010 The most popular seek for the number of bedrooms in Singapore is 4, followed by 2 and three. Lush Acres EC @ Sengkang

    Discover out more about real estate funding in the area, together with info on international funding incentives and property possession. Many Singaporeans have been investing in property across the causeway in recent years, attracted by comparatively low prices. However, those who need to exit their investments quickly are likely to face significant challenges when trying to sell their property – and could finally be stuck with a property they can't sell. Career improvement programmes, in-house valuation, auctions and administrative help, venture advertising and marketing, skilled talks and traisning are continuously planned for the sales associates to help them obtain better outcomes for his or her shoppers while at Knight Frank Singapore. No change Present Rules

    Extending the tax exemption would help. The exemption, which may be as a lot as $2 million per family, covers individuals who negotiate a principal reduction on their existing mortgage, sell their house short (i.e., for lower than the excellent loans), or take part in a foreclosure course of. An extension of theexemption would seem like a common-sense means to assist stabilize the housing market, but the political turmoil around the fiscal-cliff negotiations means widespread sense could not win out. Home Minority Chief Nancy Pelosi (D-Calif.) believes that the mortgage relief provision will be on the table during the grand-cut price talks, in response to communications director Nadeam Elshami. Buying or promoting of blue mild bulbs is unlawful.

    A vendor's stamp duty has been launched on industrial property for the primary time, at rates ranging from 5 per cent to 15 per cent. The Authorities might be trying to reassure the market that they aren't in opposition to foreigners and PRs investing in Singapore's property market. They imposed these measures because of extenuating components available in the market." The sale of new dual-key EC models will even be restricted to multi-generational households only. The models have two separate entrances, permitting grandparents, for example, to dwell separately. The vendor's stamp obligation takes effect right this moment and applies to industrial property and plots which might be offered inside three years of the date of buy. JLL named Best Performing Property Brand for second year running

    The data offered is for normal info purposes only and isn't supposed to be personalised investment or monetary advice. Motley Fool Singapore contributor Stanley Lim would not personal shares in any corporations talked about. Singapore private home costs increased by 1.eight% within the fourth quarter of 2012, up from 0.6% within the earlier quarter. Resale prices of government-built HDB residences which are usually bought by Singaporeans, elevated by 2.5%, quarter on quarter, the quickest acquire in five quarters. And industrial property, prices are actually double the levels of three years ago. No withholding tax in the event you sell your property. All your local information regarding vital HDB policies, condominium launches, land growth, commercial property and more

    There are various methods to go about discovering the precise property. Some local newspapers (together with the Straits Instances ) have categorised property sections and many local property brokers have websites. Now there are some specifics to consider when buying a 'new launch' rental. Intended use of the unit Every sale begins with 10 p.c low cost for finish of season sale; changes to 20 % discount storewide; follows by additional reduction of fiftyand ends with last discount of 70 % or extra. Typically there is even a warehouse sale or transferring out sale with huge mark-down of costs for stock clearance. Deborah Regulation from Expat Realtor shares her property market update, plus prime rental residences and houses at the moment available to lease Esparina EC @ Sengkang
  17. One of the biggest reasons investing in a Singapore new launch is an effective things is as a result of it is doable to be lent massive quantities of money at very low interest rates that you should utilize to purchase it. Then, if property values continue to go up, then you'll get a really high return on funding (ROI). Simply make sure you purchase one of the higher properties, reminiscent of the ones at Fernvale the Riverbank or any Singapore landed property Get Earnings by means of Renting

    In its statement, the singapore property listing - website link, government claimed that the majority citizens buying their first residence won't be hurt by the new measures. Some concessions can even be prolonged to chose teams of consumers, similar to married couples with a minimum of one Singaporean partner who are purchasing their second property so long as they intend to promote their first residential property. Lower the LTV limit on housing loans granted by monetary establishments regulated by MAS from 70% to 60% for property purchasers who are individuals with a number of outstanding housing loans on the time of the brand new housing purchase. Singapore Property Measures - 30 August 2010 The most popular seek for the number of bedrooms in Singapore is 4, followed by 2 and three. Lush Acres EC @ Sengkang

    Discover out more about real estate funding in the area, together with info on international funding incentives and property possession. Many Singaporeans have been investing in property across the causeway in recent years, attracted by comparatively low prices. However, those who need to exit their investments quickly are likely to face significant challenges when trying to sell their property – and could finally be stuck with a property they can't sell. Career improvement programmes, in-house valuation, auctions and administrative help, venture advertising and marketing, skilled talks and traisning are continuously planned for the sales associates to help them obtain better outcomes for his or her shoppers while at Knight Frank Singapore. No change Present Rules

    Extending the tax exemption would help. The exemption, which may be as a lot as $2 million per family, covers individuals who negotiate a principal reduction on their existing mortgage, sell their house short (i.e., for lower than the excellent loans), or take part in a foreclosure course of. An extension of theexemption would seem like a common-sense means to assist stabilize the housing market, but the political turmoil around the fiscal-cliff negotiations means widespread sense could not win out. Home Minority Chief Nancy Pelosi (D-Calif.) believes that the mortgage relief provision will be on the table during the grand-cut price talks, in response to communications director Nadeam Elshami. Buying or promoting of blue mild bulbs is unlawful.

    A vendor's stamp duty has been launched on industrial property for the primary time, at rates ranging from 5 per cent to 15 per cent. The Authorities might be trying to reassure the market that they aren't in opposition to foreigners and PRs investing in Singapore's property market. They imposed these measures because of extenuating components available in the market." The sale of new dual-key EC models will even be restricted to multi-generational households only. The models have two separate entrances, permitting grandparents, for example, to dwell separately. The vendor's stamp obligation takes effect right this moment and applies to industrial property and plots which might be offered inside three years of the date of buy. JLL named Best Performing Property Brand for second year running

    The data offered is for normal info purposes only and isn't supposed to be personalised investment or monetary advice. Motley Fool Singapore contributor Stanley Lim would not personal shares in any corporations talked about. Singapore private home costs increased by 1.eight% within the fourth quarter of 2012, up from 0.6% within the earlier quarter. Resale prices of government-built HDB residences which are usually bought by Singaporeans, elevated by 2.5%, quarter on quarter, the quickest acquire in five quarters. And industrial property, prices are actually double the levels of three years ago. No withholding tax in the event you sell your property. All your local information regarding vital HDB policies, condominium launches, land growth, commercial property and more

    There are various methods to go about discovering the precise property. Some local newspapers (together with the Straits Instances ) have categorised property sections and many local property brokers have websites. Now there are some specifics to consider when buying a 'new launch' rental. Intended use of the unit Every sale begins with 10 p.c low cost for finish of season sale; changes to 20 % discount storewide; follows by additional reduction of fiftyand ends with last discount of 70 % or extra. Typically there is even a warehouse sale or transferring out sale with huge mark-down of costs for stock clearance. Deborah Regulation from Expat Realtor shares her property market update, plus prime rental residences and houses at the moment available to lease Esparina EC @ Sengkang
  18. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  19. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  20. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  21. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  22. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  23. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  24. ISO 8807, Language of Temporal Ordering Specification
  25. 55 years old Systems Administrator Antony from Clarence Creek, really loves learning, PC Software and aerobics. Likes to travel and was inspired after making a journey to Historic Ensemble of the Potala Palace.

    You can view that web-site... ccleaner free download
  26. Origins of Go concurrency style. Talk by Rob Pike at OSCON's Emerging Languages Camp 2010.
  27. [1]. Control.Concurrent.MVar