Refer Proceedings details

%T CPA Survival Guide
%A Herman Roebbers
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X For those new to CPA, this may be helpful to get an overview
   of what the various acronyms used during the conference mean
   and how they are related. This talk should provide you with
   a good start of the conference.

%T An Overview of ASD \- Formal Methods in Daily Use
%A Guy Broadfoot
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Analytical Software Design (ASD) is an example of how formal
   methods can be introduced into the industrial workplace and
   routinely used on a daily basis. In this talk, I will give a
   quick overview of the underlying concepts and techniques
   employed.

%T occam on the Arduino
%A Adam T. Sampson, Matthew C. Jadud, Christian L. Jacobsen
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X The Arduino is an open\-source \[dq]physical computing\[dq]
   development system with a large, active user community.
   Arduino applications are usually developed in a subset of
   C++ with no concurrency facilities, which makes it difficult
   to build systems that must respond to a variety of external
   stimuli. We present an implementation of occam for
   the Arduino based on the Transterpreter portable runtime,
   adapted to make efficient use of the small
   Harvard\-architecture microcontrollers typically used on
   devices like the Arduino. In addition, we describe the
   library of processes \-\- \[dq]Plumbing\[dq] \-\- that we
   provide to ease the development of physical computing
   applications.

%T Use of Formal Models in Model\-driven Design of Embedded software
%A Oguzcan Oguz, Jan F. Broenink
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009

%T Concurrency First (but we\[rs]d better get it right!)
%A Peter H. Welch
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X This talk considers how and when concurrency should be
   taught in an undergraduate curriculum. It is to provoke
   discussion, which may later (if there is interest) become a
   theme for the Panel Session at the end of the conference
   (Wednesday morning). My presentation will focus on what we
   are doing at Kent (where concurrency has been taught as a
   full module for the past 23 years). Our belief is that
   concurrency is fundamental to most aspects of computer
   science (regardless of the push arising from the onset of
   multicore processors). It can and should be taught at the
   beginning at the same time as and a necessary and
   natural complement to sequential programming. But the
   concurrency model being taught better be right ... and
   threads\-and\-locks won\[rs]t hack it!

%T Clocks
%A Adam T. Sampson, Neil C.C. Brown
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X As part of the CoSMoS project, we have implemented a variety
   of complex systems simulations using occam\-pi. occam\-pi is
   unusual in that it provides built\-in support for
   synchronisation against a real\-time clock, but simulations
   generally need to run faster or slower than real time. We
   describe the idea of a \[dq]clock\[dq] \-\- a
   new synchronisation primitive for process\-oriented
   programming, similar to a barrier but extended with a sense
   of time. Clocks can be used to provide simulated time in a
   complex systems simulation, and can also be used to
   implement efficient phase synchronisation for
   controlling access to shared resources.

%T Traces for Testing
%A Neil C.C. Brown
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X CHP, the Haskell concurrency library, has recently
   been augmented with new testing capabilities. When a test
   case fails, its recorded event traces are automatically
   printed out \-\- with support for CSP, VCR and Structural
   trace styles.

%T A Study Into the Modelling and Analysis of Real\-Time FPGA Based Systems
%A Irfan Mir
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X High\-integrity systems are those where failure can cause
   loss of life, injury, environmental damage or financial
   loss. The reliability of these systems is very important, so
   we need verification techniques that ensure the reliability
   and understanding of these systems. The aim of this research
   is to develop techniques and a tool for verifying real\-time
   constraints in high level languages for FPGA
   based high\-integrity systems. Further a novel methodology
   using Timed CSP is to be proposed to ensure the temporal
   correctness of these systems. The outcome of this research
   is to design the constraint meta\-language and implement a
   tool which automates the analysis and verification process.
   Further this research will investigate the implementation
   of Timed CSP in Handel\-C, augmented with the constraint
   meta\-language.

%T Systems Modelling and Integration
%A Dan Slipper
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X As systems increase in complexity and become combinations of
   hardware, software and physical components, the methods of
   integrating these become difficult. In safety critical
   systems, reliability is a key factor so we want faults to be
   predictable or mitigated wherever possible. This research
   aims to discover techniques of applying formal methods for
   software to a full system incorporating hardware and
   physical components, expecting to result in improvements in
   the way interfaces are defined, such that updates and
   maintenance in the system will not affect its reliability or
   performance. Another aim alongside this is to review the
   processes followed in industry throughout the design and
   development cycle, to find methods of keeping focus
   on meeting the requirements along all stages of the process.

%T Hardware/Software Co\-Design Language Development, An EngD Introduction
%A Alex Cole
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X A short introduction to a new Engineering Doctorate and
   planned areas of study. This presentation covers a bit of
   basic background, an overview of the whole research topic
   and lists a few proposed projects, looking in some minor
   detail at one specifically.

%T Robust Robot Software using Process Orientation
%A Cagri Yalcin, Jan F. Broenink
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009

%T Beyond Mobility \- What Next After CSP/pi?
%A Michael Goldsmith
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Process algebras like CSP and CCS inspired the original
   occam model of communication and process encapsulation.
   Later the pi\-calculus and various treatments handling
   mobility in CSP added support for mobility, as realised in
   practical programming systems such as occam\-pi, JCSP, CHP
   and Sufrin\[rs]s CSO, which allow a rather abstract notion
   of motion of processes and channel ends between parents
   or owners. Milner\[rs]s Space and Motion of Communicating
   Agents on the other hand describes the bigraph framework,
   which makes location more of a first\-class citizen of the
   calculus and evolves through reaction rules which rewrite
   both place and link graphs of matching sections of a system
   state, allowing more dramatic dynamic reconfigurations of a
   system than simple process spawning or migration. I consider
   the tractability of the notation, and to what extent the
   additional flexibility reflects or elicits
   desirable programming paradigms.

%T The SCOOP Concurrency Model in Java\-like Languages
%A Faraz Torshizi, Jonathan S. Ostroff, Richard F. Paige, Marsha Chechik
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X SCOOP is a minimal extension to the sequential
   object\-oriented programming model for concurrency. The
   extension consists of one keyword (separate) that avoids
   explicit thread declarations, synchronized blocks, explicit
   waits, and eliminates data races and atomicity violations by
   construction, through a set of compiler rules. SCOOP was
   originally described for the Eiffel programming
   language. This paper makes two contributions. Firstly, it
   presents a design pattern for SCOOP, which makes it feasible
   to transfer SCOOP\[rs]s concepts to different
   object\-oriented programming languages. Secondly, it
   demonstrates the generality of the SCOOP model by presenting
   an implementation of the SCOOP design pattern for
   Java. Additionally, we describe tools that support the SCOOP
   design pattern, and give a concrete example of its use in
   Java.

%T Combining Partial Order Reduction with Bounded Model Checking
%A José Vander Meulen, Charles Pecheur
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Model checking is an efficient technique for verifying
   properties on reactive systems. Partial\-order reduction
   (POR) and symbolic model checking are two common approaches
   to deal with the state space explosion problem in model
   checking. Traditionally, symbolic model checking uses BDDs
   which can suffer from space blow\-up. More recently bounded
   model checking (BMC) using SAT\-based procedures has been
   used as a very successful alternative to BDDs. However,
   this approach gives poor results when it is applied to
   models with a lot of asynchronism. This paper presents an
   algorithm which combines partial order reduction methods and
   bounded model checking techniques in an original way that
   allows efficient verification of temporal logic properties
   (LTL_X) on models featuring asynchronous processes. The
   encoding to a SAT problem strongly reduces the complexity
   and non\-determinism of each transition step, allowing
   efficient analysis even with longer execution traces. The
   starting\-point of our work is the Two\-Phase algorithm
   (Namalesu and Gopalakrishnan) which performs partial\-order
   reduction on process\-based models. At first, we adapt this
   algorithm to the bounded model checking method. Then, we
   describe our approach formally and demonstrate its validity.
   Finally, we present a prototypal implementation and report
   encouraging experimental results on a small example.

%T On Congruence Property of Scope Equivalence for Concurrent Programs with Higher\-Order Communication
%A Masaki Murakami
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Representation of scopes of names is important for analysis
   and verification of concurrent systems. However, it is
   difficult to represent the scopes of channel names precisely
   with models based on process algebra. We introduced a model
   of concurrent systems with higher\-order communication based
   on graph rewriting in our previous work. A bipartite
   directed acyclic graph represents a concurrent system that
   consists of a number of processes and messages in
   that model. The model can represent the scopes of local
   names precisely. We defined an equivalence relation such
   that two systems are equivalent not only in their behavior
   but in extrusion of scopes of names. This paper shows that
   the equivalence relation is a congruence relation wrt
   tau\-prefix, new\-name, replication and composition even if
   higher\-order communication is allowed. And we also show
   the equivalence relation is not congruent wrt
   input\-prefix though it is congruent wrt input prefix in
   first\-order case.

%T Analysing gCSP Models Using Runtime and Model Analysis Algorithms
%A Maarten M. Bezemer, Marcel A. Groothuis, Jan F. Broenink
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X This paper presents two algorithms for analysing gCSP models
   in order to improve their execution performance. Designers
   tend to create many small separate processes for each task,
   which results in many (resource intensive) context switches.
    The research challenge is to convert the model created from
   a design point of view to models which have better
   performance during execution, without limiting the designers
   in their ways of working. The first algorithm analyses
   the model during run\-time execution in order to find static
   sequential execution traces that allow for optimisation.
   The second algorithm analyses the gCSP model for multi\-core
   execution. It tries to find a resource\-efficient placement
   on the available cores for the given target systems. Both
   algorithms are implemented in two tools and are tested. We
   conclude that both algorithms complement each other and the
   analysis results are suitable to create optimised models.

%T Relating and Visualising CSP, VCR and Structural Traces
%A Neil C.C. Brown, Marc L. Smith
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X As well as being a useful tool for formal reasoning, a trace
   can provide insight into a concurrent program\[rs]s
   behaviour, especially for the purposes of run\-time analysis
   and debugging. Long\-running programs tend to produce large
   traces which can be difficult to comprehend and visualise.
   We examine the relationship between three types of traces
   (CSP, VCR and Structural), establish an ordering
   and describe methods for conversion between the trace types.
    Structural traces preserve the structure of composition and
   reveal the repetition of individual processes, and are thus
   well\-suited to visualisation. We introduce the Starving
   Philosophers to motivate the value of structural traces for
   reasoning about behaviour not easily predicted from a
   program\[rs]s specification. A remaining challenge is to
   integrate structural traces into a more formal setting, such
   as the Unifying Theories of Programming \-\- however,
   structural traces do provide a useful framework for
   analysing large systems.

%T Designing a Mathematically Verified I2C Device Driver using ASD
%A Arjen Klomp, Herman Roebbers, Ruud Derwig, Leon Bouwmeester
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X This paper describes the application of the Analytical
   Software Design methodology to the development of a
   mathematically verified I2C device driver for Linux. A model
   of an I2C controller from NXP is created, against which the
   driver component is modelled. From within the ASD tool the
   composition is checked for deadlock, livelock and
   other concurrency issues by generating CSP from the models
   and checking these models with the CSP model checker FDR.
   Subsequently C code is automatically generated which, when
   linked with a suitable Linux kernel run\-time, provides a
   complete defect\-free Linux device driver. The performance
   and footprint are comparable to handwritten code.

%T Mobile Escape Analysis for occam\-pi
%A Frederick R. M. Barnes
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Escape analysis is the process of discovering boundaries
   of dynamically allocated objects in programming languages.
   For object\-oriented languages such as C++ and Java, this
   analysis leads to an understanding of which program objects
   interact directly, as well as what objects hold references
   to other objects. Such information can be used to help
   verify the correctness of an implementation with respect to
   its design, or provide information to a run\-time
   system about which objects can be allocated on the stack
   (because they do not \[dq]escape\[dq] the method in which
   they are declared). For existing object\-oriented
   languages, this analysis is typically made difficult by
   aliasing endemic to the language, and is further complicated
   by inheritance and polymorphism. In contrast, the occam\-pi
   programming language is a process\-oriented language, with
   systems built from layered networks of communicating
   concurrent processes. The language has a strong
   relationship with the CSP process algebra, that can be used
   to reason formally about the correctness of occam\-pi
   programs. This paper presents early work on a compositional
   escape analysis technique for mobiles in the occam\-pi
   programming language, in a style not dissimilar to existing
   CSP analyses. The primary aim is to discover the boundaries
   of mobiles within the communication graph, and to determine
   whether or not they escape any particular process or network
   of processes. The technique is demonstrated by analysing
   some typical occam\-pi processes and networks, giving a
   formal understanding of their mobile escape behaviour.

%T New ALT for Application Timers and Synchronisation Point Scheduling
%A Øyvind Teig, Per Johan Vannebo
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X During the design of a small channel\-based concurrency
   runtime system (ChanSched, written in ANSI C), we saw that
   application timers (which we call egg and repeat timers)
   could be part of its supported ALT construct, even if their
   states live through several ALTs. There are no side effects
   into the ALT semantics, which enable waiting for channels,
   channel timeout and, now, the new application
   timers. Application timers are no longer busy polled for
   timeout by the process. We show how the classical occam
   language may benefit from a spin\-off of this same idea.
   Secondly, we wanted application programmers to be freed from
   their earlier practice of explicitly coding communication
   states at channel synchronisation points, which was needed
   by a layered in\-house scheduler. This led us to develop
   an alternative to the non\-ANSI C \[dq]computed goto\[dq]
   (found in gcc). Instead, we use a switch/case with goto
   line\-number\-tags in a synch\-point\-table for scheduling.
   We call this table, one for each process, a proctor table.
   The programmer does not need to manage this table, which
   is generated with a script, and hidden within an
   \[sh]include file.

%T Translating ETC to LLVM Assembly
%A Carl G. Ritson
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X The LLVM compiler infrastructure project provides a
   machine independent virtual instruction set, along with
   tools for its optimisation and compilation to a wide range
   of machine architectures. Compiler writers can use the
   LLVM\[rs]s tools and instruction set to simplify the task of
   supporting multiple hardware/software platforms. In this
   paper we present an exploration of translation
   from stack\-based Extended Transputer Code (ETC) to
   SSA\-based LLVM assembly language. This work is intended to
   be a stepping stone towards direct compilation of occam\-pi
   and similar languages to LLVM\[rs]s instruction set.

%T Resumable Java Bytecode \- Process Mobility for ProcessJ targeting the JVM
%A Jan Bækgaard Pedersen, Brian Kauke
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X This paper describes an implementation of resumable and
   mobile processes for a new process\-oriented language called
   ProcessJ. ProcessJ is based on CSP and the pi\-calculus; it
   is structurally very close to occam\-pi, but the syntax is
   much closer to the imperative part of Java (with new
   constructs added for process orientation). One of the
   targets of ProcessJ is Java bytecode to be executed on the
   Java Virtual Machine (JVM), and in this paper we describe
   how to implement the process mobility features of ProcessJ
   with respect to the Java Virtual Machine. We show how to add
   functionality to support resumability (and process mobility)
   by a combination of code rewriting (adding extra code to the
   generated Java target code), as well as bytecode rewriting.

%T OpenComRTOS: A Runtime Environment for Interacting Entities
%A Bernhard H.C. Sputh, Oliver Faust, Eric Verhulst, Vitaliy Mezhuyev
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X OpenComRTOS is one of the few Real\-Time Operating Systems
   for embedded systems that was developed using formal
   modelling techniques. The goal was to obtain a proven
   dependable component with a clean architecture that delivers
   high performance on a wide variety of networked
   embedded systems, ranging from a single processor to
   distributed systems. The result is a scalable relibable
   communication system with real\-time capabilities. Besides,
   a rigorous formal verification of the kernel algorithms led
   to an architecture which has several properties that enhance
   safety and real\-time properties of the RTOS. The code size
   in particular is very small, typically 10 times less than a
   typical equivalent single processor RTOS. The small code
   size allows a much better use of the on\-chip memory
   resources, which increases the speed of execution due to the
   reduction of wait states caused by the use of external
   memory. To this point we ported OpenComRTOS to
   the MicroBlaze processor from Xilinx, the Leon3 from ESA,
   the ARM Cortex\-M3, the Melexis MLX16, and the XMOS. In this
   paper we concentrate on the Microblaze port, which is an
   environment where OpenComRTOS competes with a number of
   different operating systems, including the standard
   operating system Xilinx Micro Kernel. This paper reports
   code size figures of the OpenComRTOS on a MicroBlaze target.
   We found that this code size is considerably smaller
   compared with published code sizes of other operating
   systems.

%T Economics of Cloud Computing: a Statistical Genetics Case Study
%A Jeremy M. R. Martin, Steven J. Barrett, Simon J. Thornber, Silviu-Alin Bacanu, Dale Dunlap, Steve Weston
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X We describe an experiment which aims to reduce significantly
   the costs of running a particular large\-scale grid\-enabled
   application using commercial cloud computing resources. We
   incorporate three tactics into our experiment: improving the
   serial performance of each work unit, seeking the most
   cost\-effective computation cycles, and making use of an
   optimized resource manager and scheduler. The
   application selected for this work is a genetics association
   analysis and is representative of a common class of
   embarrassingly parallel problems.

%T An Application of CoSMoS Design Methods to Pedestrian Simulation
%A Sarah Clayton, Neil Urquhart, Jon Kerridge
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X In this paper, we discuss the implementation of a simple
   pedestrian simulation that uses a multi agent based design
   pattern developed by the CoSMoS research group. Given the
   nature of Multi Agent Systems (MAS), parallel processing
   techniques are inevitably used in their implementation. Most
   of these approaches rely on conventional
   parallel programming techniques, such as threads, Message
   Passing Interface (MPI) and Remote Method Invocation (RMI).
   The CoSMoS design patterns are founded on the use of
   Communicating Sequential Processes (CSP), a parallel
   computing paradigm that emphasises a process oriented
   rather than object oriented programming perspective.

%T An Investigation into Distributed Channel Mobility Support for Communicating Process Architectures
%A Kevin Chalmers, Jon Kerridge
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Localised mobile channel support is now a feature of
   Communicating Process Architecture (CPA) based frameworks,
   from JCSP and C++CSP to occam\-pi. Distributed mobile
   channel support has also been attempted in JCSP Networking
   and occam\-pi via the pony framework, although
   the capabilities of these two separate approaches is limited
   and has not led to the widespread usage of distributed
   mobile channel primitives. In this paper, an initial
   investigation into possible models that can support
   distributed channel mobility are presented and analysed
   for features such as transmission time, robustness and
   reachability. The goal of this work is to discover a set of
   models which can be used for channel mobility and also
   supported within the single unified protocol for distributed
   CPA frameworks. From the analysis presented in this paper,
   it has been determined that there are models which can
   be implemented to support channel end mobility within a
   single unified protocol which provide suitable capabilities
   for certain application scenarios.

%T Auto\-Mobiles: Optimised Message\-Passing
%A Neil C.C. Brown
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Some message\-passing concurrent systems, such as occam 2,
   prohibit aliasing of data objects. Communicated data must
   thus be copied, which can be time\-intensive for large data
   packets such as video frames. We introduce automatic
   mobility, a compiler optimisation that performs
   communications by reference and deduces when
   these communications can be performed without copying. We
   discuss bounds for speed\-up and memory use, and benchmark
   the automatic mobility optimisation. We show that in the
   best case it can transform an operation from being linear
   with respect to packet size into constant\-time.

%T A Denotational Study of Mobility
%A Joël-Alexis Bialkiewicz, Frederic Peschanski
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X This paper introduces a denotational model and refinement
   theory for a process algebra with mobile channels. Similarly
   to CSP, process behaviours are recorded as trace sets. To
   account for branching\-time semantics, the traces are
   decorated by structured locations that are also used to
   encode the dynamics of channel mobility in a
   denotational way. We present an original notion of
   split\-equivalence based on elementary trace
   transformations. It is first characterised coinductively
   using the notion of split\-relation. Building on
   the principle of trace normalisation, a more denotational
   characterisation is also proposed. We then exhibit a
   preorder underlying this equivalence and motivate its use as
   a proper refinement operator. At the language level, we show
   refinement to be tightly related to a construct of delayed
   sums, a generalisation of non\-deterministic choices.

%T PyCSP Revisited
%A Brian Vinter, John Markus Bjørndalen, Rune Møllegard Friborg
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X PyCSP was introduced two years ago and has since been used
   by a number of programmers, especially students. The
   original motivation behind PyCSP was a conviction that both
   Python and CSP are tools that are especially well suited for
   programmers and scientists in other fields than computer
   science. Working under this premise the original PyCSP was
   very similar to JCSP and the motivation was simply to
   provide CSP to the Python community in the JCSP tradition.
   After two years we have concluded that PyCSP is indeed a
   usable tool for the target users; however many of them have
   raised some of the same issues with PyCSP as with JCSP. The
   many channel types, lack of output guards and
   external choice wrapped in the select\-then\-execute
   mechanism were frequent complaints. In this work we revisit
   PyCSP and address the issues that have been raised. The
   result is a much simpler PyCSP with only one channel type,
   support for output guards, and external choice that
   is closer to that of occam than JCSP.

%T Three Unique Implementations of Processes for PyCSP
%A Rune Møllegard Friborg, John Markus Bjørndalen, Brian Vinter
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X In this work we motivate and describe three unique
   implementations of processes for PyCSP: process, thread and
   greenlet based. The overall purpose is to demonstrate the
   feasibility of Communicating Sequential Processes as a
   framework for different application types and
   target platforms. The result is a set of three
   implementations of PyCSP with identical interfaces to the
   point where a PyCSP developer need only change which
   implementation is imported to switch to any of the
   other implementations. The three implementations have
   different strengths; processes favors parallel processing,
   threading portability and greenlets favor many processes
   with frequent communication. The paper includes examples of
   applications in all three categories.

%T CSP as a Domain\-Specific Language Embedded in Python and Jython
%A Sarah Mount, Mohammad Hammoudeh, Sam Wilson, Robert Newman
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Recently, much discussion has taken place within the
   Python programming community on how best to support
   concurrent programming. This paper describes a new Python
   library, python\-csp, which implements synchronous,
   message\-passing concurrency based on
   Hoare\[rs]s Communicating Sequential Processes. Although
   other CSP libraries have been written for Python,
   python\-csp has a number of novel features. The library is
   implemented both as an object hierarchy and as
   a domain\-specific language, meaning that programmers can
   compose processes and guards using infix operators, similar
   to the original CSP syntax. The language design is intended
   to be idiomatic Python and is therefore quite different to
   other CSP libraries. python\-csp targets the CPython
   interpreter and has variants which reify CSP process as
   Python threads and operating system processes. An equivalent
   library targets the Jython interpreter, where CSP
   processes are reified as Java threads. jython\-csp also has
   Java wrappers which allow the library to be used from pure
   Java programs. We describe these aspects of python\-csp,
   together with performance benchmarks and a formal analysis
   of channel synchronisation and choice, using the model
   checker SPIN.

%T Hydra: A Python Framework for Parallel Computing
%A Waide B. Tristram, Karen Bradshaw
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X This paper investigates the feasibility of developing a CSP
   to Python translator using a concurrent framework for
   Python. The objective of this translation framework,
   developed under the name of Hydra, is to produce a tool that
   helps programmers implement concurrent software easily using
   CSP algorithms. This objective was achieved using the ANTLR
   compiler generator tool, Python Remote Objects and PyCSP.
   The resulting Hydra prototype takes an algorithm defined in
   CSP, parses and converts it to Python and then executes the
   program using multiple instances of the Python interpreter.
   Testing has revealed that the Hydra prototype appears to
   function correctly, allowing simultaneous process execution.
   Therefore, it can be concluded that converting CSP to Python
   using a concurrent framework such as Hydra is both
   possible and adds flexibility to CSP with embedded Python
   statements.

%T Extending CSP with Tests for Availability
%A Gavin Lowe
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X We consider the language of CSP extended with a construct
   that allows processes to test whether a particular event is
   available (without actually performing the event). We
   present an operational semantics for this language, together
   with two congruent denotational semantic models. We also
   show how this extended language can be simulated using
   standard CSP, so as to be able to analyse systems using
   the model checker FDR.

%T Design Patterns for Communicating Systems with Deadline Propagation
%A Martin Korsgaard, Sverre Hendseth
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Toc is an experimental programming language based on occam
   that combines CSP\-based concurrency with integrated
   specification of timing requirements. In contrast to occam
   with strict round\-robin scheduling, the Toc scheduler is
   lazy and does not run a process unless there is a deadline
   associated with its execution. Channels propagate
   deadlines to dependent tasks. These differences from occam
   necessitate a different approach to programming, where a new
   concern is to avoid dependencies and conflicts between
   timing requirements. This paper introduces client\-server
   design patterns for Toc that allow the programmer precise
   control of timing. It is shown that if these patterns are
   used, the deadline propagation graph can be used to provide
   sufficient conditions for schedulability. An
   alternative definition of deadlock in deadline\-driven
   systems is given, and it is demonstrated how the use of the
   suggested design patterns allow the absence of deadlock to
   be proven in Toc programs. The introduction of extended
   rendezvous into Toc is shown to be essential to
   these patterns.

%T JCSP Agents\-Based Service Discovery for Pervasive Computing
%A Anna Kosek, Jon Kerridge, Aly Syed, Alistair Armitage
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Device and service discovery is a very important topic
   when considering pervasive environments. The discovery
   mechanism is required to work in networks with dynamic
   topology and on limited software, and be able to accept
   different device descriptions. This paper presents a service
   and device discovery mechanism using JCSP agents and the
   JCSP network package jcsp.net2.

%T Toward Process Architectures for Behavioural Robotics
%A Jonathan Simpson, Carl G. Ritson
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Building robot control programs which function as intended
   is a challenging task. Roboticists have developed
   architectures to provide principles, constraints and
   primitives which simplify the building of these correct,
   well structured systems. A number of established
   and prevalent behavioural architectures for robot control
   make use of explicit parallelism with message passing.
   Expressing these architectures in terms of a
   process\-oriented programming language, such as occam\-pi,
   allows us to distil design rules, structures and primitives
   for use in the development of process architectures
   for robot control.

%T HW/SW Design Space Exploration on the Production Cell Setup
%A Marcel A. Groothuis, Jan F. Broenink
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X This paper describes and compares five CSP based and two CSP
   related process\-oriented motion control system
   implementations that are made for our Production Cell
   demonstration setup. Five implementations
   are software\-based and two are FPGA hardware\-based. All
   implementations were originally made with different purposes
   and investigating different areas of the design space for
   embedded control software resulting in an interesting
   comparison between approaches, tools and software and
   hardware implementations. Common for all implementations is
   the usage of a model\-driven design method, a communicating
   process structure, the combination of discrete event and
   continuous time and that real\-time behaviour is essential.
   This paper shows that many small decisions made during the
   design of all these embedded control software
   implementations influence our route through the design
   space for the same setup, resulting in seven different
   solutions with different key properties. None of the
   implementations is perfect, but they give us valuable
   information for future improvements of our design methods
   and tools.

%T Engineering Emergence: an occam\-pi Adventure
%A Peter H. Welch, Kurt Wallnau, Mark Klein
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Future systems will be too complex to design and implement
   explicitly. Instead, we will have to learn to engineer
   complex behaviours indirectly: through the discovery and
   application of local rules of behaviour, applied to simple
   process components, from which desired behaviours
   predictably emerge through dynamic interactions
   between massive numbers of instances. This talk considers
   such indirect engineering of emergence using a
   process\-oriented architecture. Different varieties of
   behaviour may emerge within a single application, with
   interactions between them provoking ever\-richer patterns
   almost social systems. We will illustrate with a study based
   on Reynolds\[rs] boids: emergent behaviours include flocking
   (of course), directional migration (with waves), fear and
   panic (of hawks), orbiting (points of interest), feeding
   frenzy (when in a large enough flock), turbulent flow and
   maze solving. With this kind of engineering, a new problem
   shows up: the suppression of the emergence of undesired
   behaviours. The panic reaction within a flock to the sudden
   appearance of a hawk is a case in point. With our
   present rules, the flock loses cohesion and scatters too
   quickly, making individuals more vulnerable. What are the
   rules that will make the flock turn almost\-as\-one and
   maintain most of its cohesion? There are only the boids to
   which these rules may apply (there being, of course, no
   design or programming entity corresponding to a flock).
   More importantly, how do we set about finding such rules in
   the first place? Our architecture and models are written in
   occam\-pi, whose processes are sufficiently lightweight to
   enable a sufficiently large mass to run and be interacted
   with for real\-time experiments on emergent behaviour. This
   work is in collaboration with the Software Engineering
   Institute (at CMU) and is part of the CoSMoS project (at the
   Universities of Kent and York in the UK).

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.