Proceedings details
Title: Communicating Process Architectures 2009
Editors: Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
Publisher: IOS Press, Amsterdam
ISBN: 978-1-60750-065-0
ISSN: 1383-7575
Keynote presentations
| Title: |
Beyond Mobility - What Next After CSP/pi?
|
| Authors: |
Michael Goldsmith |
| Abstract: |
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's CSO, which allow a rather abstract
notion of motion of processes and channel ends between parents or
owners. Milner'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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
Papers
| Title: |
The SCOOP Concurrency Model in Java-like Languages
|
| Authors: |
Faraz Torshizi, Jonathan S. Ostroff, Richard F. Paige, Marsha Chechik |
| Abstract: |
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'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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Combining Partial Order Reduction with Bounded Model Checking
|
| Authors: |
José Vander Meulen, Charles Pecheur |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
On Congruence Property of Scope Equivalence for Concurrent Programs with Higher-Order Communication
|
| Authors: |
Masaki Murakami |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Analysing gCSP Models Using Runtime and Model Analysis Algorithms
|
| Authors: |
Maarten M. Bezemer, Marcel A. Groothuis, Jan F. Broenink |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Relating and Visualising CSP, VCR and Structural Traces
|
| Authors: |
Neil C.C. Brown, Marc L. Smith |
| Abstract: |
As well as being a useful tool for formal reasoning, a trace can
provide insight into a concurrent program'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'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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Designing a Mathematically Verified I2C Device Driver using ASD
|
| Authors: |
Arjen Klomp, Herman Roebbers, Ruud Derwig, Leon Bouwmeester |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Mobile Escape Analysis for occam-pi
|
| Authors: |
Frederick R. M. Barnes |
| Abstract: |
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
"escape" 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
New ALT for Application Timers and Synchronisation Point Scheduling
|
| Authors: |
Øyvind Teig, Per Johan Vannebo |
| Abstract: |
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 "computed goto" (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 #include file. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Translating ETC to LLVM Assembly
|
| Authors: |
Carl G. Ritson |
| Abstract: |
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'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's instruction
set. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Resumable Java Bytecode - Process Mobility for ProcessJ targeting the JVM
|
| Authors: |
Jan Bækgaard Pedersen, Brian Kauke |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
OpenComRTOS: A Runtime Environment for Interacting Entities
|
| Authors: |
Bernhard H.C. Sputh, Oliver Faust, Eric Verhulst, Vitaliy Mezhuyev |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Economics of Cloud Computing: a Statistical Genetics Case Study
|
| Authors: |
Jeremy M. R. Martin, Steven J. Barrett, Simon J. Thornber, Silviu-Alin Bacanu, Dale Dunlap, Steve Weston |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
An Application of CoSMoS Design Methods to Pedestrian Simulation
|
| Authors: |
Sarah Clayton, Neil Urquhart, Jon Kerridge |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
An Investigation into Distributed Channel Mobility Support for Communicating Process Architectures
|
| Authors: |
Kevin Chalmers, Jon Kerridge |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Auto-Mobiles: Optimised Message-Passing
|
| Authors: |
Neil C.C. Brown |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
A Denotational Study of Mobility
|
| Authors: |
Joël-Alexis Bialkiewicz, Frederic Peschanski |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
PyCSP Revisited
|
| Authors: |
Brian Vinter, John Markus Bjørndalen, Rune Møllegard Friborg |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Three Unique Implementations of Processes for PyCSP
|
| Authors: |
Rune Møllegard Friborg, John Markus Bjørndalen, Brian Vinter |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
CSP as a Domain-Specific Language Embedded in Python and Jython
|
| Authors: |
Sarah Mount, Mohammad Hammoudeh, Sam Wilson, Robert Newman |
| Abstract: |
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'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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Hydra: A Python Framework for Parallel Computing
|
| Authors: |
Waide B. Tristram, Karen Bradshaw |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Extending CSP with Tests for Availability
|
| Authors: |
Gavin Lowe |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Design Patterns for Communicating Systems with Deadline Propagation
|
| Authors: |
Martin Korsgaard, Sverre Hendseth |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
JCSP Agents-Based Service Discovery for Pervasive Computing
|
| Authors: |
Anna Kosek, Jon Kerridge, Aly Syed, Alistair Armitage |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Toward Process Architectures for Behavioural Robotics
|
| Authors: |
Jonathan Simpson, Carl G. Ritson |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
HW/SW Design Space Exploration on the Production Cell Setup
|
| Authors: |
Marcel A. Groothuis, Jan F. Broenink |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
Fringe presentations
| Title: |
Engineering Emergence: an occam-pi Adventure
|
| Authors: |
Peter H. Welch, Kurt Wallnau, Mark Klein |
| Abstract: |
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' 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). |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Abstract (PDF), Slides (PDF) |
| Title: |
CPA Survival Guide
|
| Authors: |
Herman Roebbers |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
An Overview of ASD - Formal Methods in Daily Use
|
| Authors: |
Guy Broadfoot |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
occam on the Arduino
|
| Authors: |
Adam T. Sampson, Matthew C. Jadud, Christian L. Jacobsen |
| Abstract: |
The Arduino is an open-source "physical computing" 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 -- "Plumbing" -- that we provide to ease the
development of physical computing applications. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Use of Formal Models in Model-driven Design of Embedded software
|
| Authors: |
Oguzcan Oguz, Jan F. Broenink |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Concurrency First (but we'd better get it right!)
|
| Authors: |
Peter H. Welch |
| Abstract: |
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't hack it! |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Clocks
|
| Authors: |
Adam T. Sampson, Neil C.C. Brown |
| Abstract: |
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 "clock" -- 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Traces for Testing
|
| Authors: |
Neil C.C. Brown |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
A Study Into the Modelling and Analysis of Real-Time FPGA Based Systems
|
| Authors: |
Irfan Mir |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Systems Modelling and Integration
|
| Authors: |
Dan Slipper |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Hardware/Software Co-Design Language Development, An EngD Introduction
|
| Authors: |
Alex Cole |
| Abstract: |
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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Robust Robot Software using Process Orientation
|
| Authors: |
Cagri Yalcin, Jan F. Broenink |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
|
