vp - A Value-Passing Translator for CCS

Process algebras are designed to capture the essense of distributed computing in a minimal fashion, so it's not surprising that they are bad for describing complex distributed systems. While at the University of Edinburgh I spent some time using CCS and temporal logic to analyze safety-critical systems, and quickly learned how painful it is to describe systems with basic CCS. One really needs the suport for data found in an extended process algebra like value-passing form of CCS. Unfortunately, many tools for process algebras, like the Edinburgh Concurrency Workbench, do not support value-passing processes. I therefore developed (with the help of Stuart Anderson) a value-passing CCS notation and a compiler to translate value-passing CCS to basic CCS. This tool is called vp. p> The value-passing language supported by vp includes the constructs defined by Robin Milner in Communication and Concurrency, plus some other features, notably indexed actions and extensions for timed CCS. For data the language supports sets, tuples, and lists, all of which are built up out of boolean, integer, and string constants. The translator can produce basic CCS in two formats: one for the Edinburgh Concurrency Workbench and the other for the Concurrency Workbench of New Jersey.

The value-passing translator is written in Standard ML of New Jersey. Binaries for Sun workstations are freely available. If you are interested in building the compiler for us on other machines, or are interested in extending the compiler, please contact me.

There is now also a Java-based version of the value-passing translator, named "jvp". A beta version of it is available for download (see below). This version is faster than the the ML version, requires no installation, and supports timed CCS. However, it currently produces output only for the Edinburgh Concurrency Workbench.

Notice: this software (both the ML and Java versions) is for educational and research purposes only. It is not to be used as the basis for commercial products.

vp files:

1. A jar file for the beta, Java-based jvp
2. Notes on using jvp.
3. A compressed binary for the ML version of vp (Sun Solaris operating system)
4. A compressed binary for the ML version of vp (Sun OS 4 operating system)
5. The vp user guide
6. The definition of value-passing CCS
7. Some vp files related to my CCS book:
• Triple-modular redundancy: model 1 and model 2
• Sift-out modular redundancy: model
• On-the-fly Garbage Collection: model 1, model 2, and properties
• MSMIE protocol: natural model, abstract model, new model, and properties
• Slowscan protocol: model 1, model 2, buffer properties, and failure properties

timed-extensions:

1. Some notes on the syntax of the timed version of value-passing CCS
2. A compressed binary for the Solaris operating system, timed version
3. An example in timed value-passing CCS