Beyond Mobility - What Next After CSP/pi?
Michael GOLDSMITH, e-Security Group, WMG Digital Laboratory, University of Warwick

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.

Mobile Escape Analysis for occam-pi
Frederick R.M. BARNES, School of Computing, University of Kent

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.

Analysing gCSP Models Using Runtime and Model Analysis Algorithms
Maarten M. BEZEMER, Marcel A. GROOTHUIS and Jan F. BROENINK, Control Engineering, Faculty EE-M-CS, University of Twente

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.

A Denotational Study of Mobility
Joël-Alexis BIALKIEWICZ and Frédéric PESCHANSKI, Artificial Intelligence Department, Laboratoire d'Informatique de Paris 6

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.

Auto-Mobiles: Optimised Message-Passing
Neil C.C. BROWN, School of Computing, University of Kent

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.

Relating and Visualising CSP, VCR and Structural Traces
Neil C.C. BROWN (a) and Marc L. SMITH (b)
(a) School of Computing, University of Kent
(b) Computer Science Department, Vassar College

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.

An Investigation into Distributed Channel Mobility Support for Communicating Process Architectures
Kevin CHALMERS and Jon KERRIDGE, School of Computing, Napier University

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.

An Application of CoSMoS Design Methods to Pedestrian Simulation
Sarah CLAYTON, School of Computing, Napier University

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.

Three Unique Implementations of Processes for PyCSP
Rune Møllegaard FRIBORG (a), John Markus BJØRNDALEN (a) and Brian VINTER (b)
(a) Department of Computer Science, University of Tromsø
(b) Department of Computer Science, University of Copenhagen

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.

HW/SW Design Space Exploration on the Production Cell Setup
Marcel A. GROOTHUIS and Jan F. BROENINK, Control Engineering, Faculty EE-M-CS, University of Twente

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.

Designing a Mathematically Verified I2C Device Driver using ASD
Arjen KLOMP (a), Herman ROEBBERS (b), Ruud DERWIG (c) and Leon BOUWMEESTER (a)
(a) Verum B.V., Waalre, The Netherlands
(b) TASS B.V., Eindhoven, The Netherlands
(c) NXP Semiconductors Research, Eindhoven, The Netherlands

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.

Design Patterns for Communicating Systems with Deadline Propagation
Martin KORSGAARD and Sverre HENDSETH, Department of Engineering Cybernetics, Norwegian University of Science and Technology

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.

JCSP Agents-Based Service Discovery for Pervasive Computing
Anna KOSEK (a), Jon KERRIDGE (a), Aly SYED (b) and Alistair ARMITAGE (a)
(a) School of Computing, Napier University
(b) NXP Semiconductors Research, Eindhoven, The Netherlands

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.

Extending CSP with Tests for Availability
Gavin LOWE, Computing Laboratory, Oxford University

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.

Economics of Cloud Computing: a Statistical Genetics Case Study
Jeremy M.R. MARTIN, Steven J. BARRETT, Simon J. THORNBER and Silviu-Alin BACANU, GlaxoSmithKline R&D Ltd.

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.

Combining Partial Order Reduction with Bounded Model Checking
José VANDER MEULEN and Charles PECHEUR, Département d'Ingénierie Informatique, Université Catholique de Louvain

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.

CSP as a Domain-Specific Language Embedded in Python and Jython
Sarah MOUNT, Mohammad HAMMOUDEH, Sam WILSON and Robert NEWMAN, School of Computing and IT, University of Wolverhampton

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.

On Congruence Property of Scope Equivalence for Concurrent Programs with Higher-Order Communication
Masaki MURAKAMI, Department of Computer Science, Okayama University

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.

Resumable Java Bytecode - Process Mobility for ProcessJ targeting the JVM
Jan B. PEDERSEN and Brian KAUKE, School of Computer Science, University of Nevada

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.

Translating ETC to LLVM Assembly
Carl G. RITSON, School of Computing, University of Kent

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.

Toward Process Architectures for Behavioural Robotics
Jonathan SIMPSON and Carl G. RITSON, School of Computing, University of Kent

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.

OpenComRTOS: A Runtime Environment for Interacting Entities
Bernhard H.C. SPUTH, Oliver FAUST, Eric VERHULST and Vitaliy MEZHUYEV, Altreonic

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.

New ALT for Application Timers and Synchronisation Point Scheduling
Øyvind TEIG and Per Johan VANNEBO, Autronica Fire and Security, Trondheim, Norway

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.

The SCOOP Concurrency Model in Java-like Languages
Faraz TORSHIZI (a), Jonathan S. OSTROFF (b), Richard F. PAIGE (c) and Marsha CHECHIK (a)
(a) Department of Computer Science, University of Toronto
(b) Department of Computer Science and Engineering, York University, Toronto
(c) Department of Computer Science, University of York

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.

Hydra: A Python Framework for Parallel Computing
Waide B. TRISTRAM and Karen BRADSHAW, Department of Computer Science, Rhodes University

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.

PyCSP Revisited
Brian VINTER (a), John Markus BJØRNDALEN (b) and Rune Møllegaard FRIBORG (b)
(a) Department of Computer Science, University of Copenhagen
(b) Department of Computer Science, University of Tromsø

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.

An Overview of ASD - Formal Methods in Daily Use
Guy BROADFOOT, Verum B.V., Waalre, The Netherlands

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.

Traces for Testing
Neil C.C. BROWN, School of Computing, University of Kent

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.

Hardware/Software Co-Design Language Development, An EngD Introduction
Alex COLE, Department of Engineering, University of Leicester

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.

A Study Into the Modelling and Analysis of Real-Time FPGA Based Systems
Irfan MIR, Department of Engineering, University of Leicester

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.

Use of Formal Models in Model-driven Design of Embedded software
Oguzcan OGUZ and Jan F. BROENINK, Control Engineering, Faculty EE-M-CS, University of Twente

CPA Survival Guide
Herman ROEBBERS, TASS B.V., Eindhoven, The Netherlands

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.

Clocks
Adam T. SAMPSON and Neil C.C. BROWN, School of Computing, University of Kent

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.

occam on the Arduino
Adam T. SAMPSON (a), Matthew C. JADUD (b) and Christian L. JACOBSEN (c)
(a) School of Computing, University of Kent
(b) Department of Computer Science, Allegheny College
(c) Department of Computer Science, University of Copenhagen

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.

Systems Modelling and Integration
Dan SLIPPER, Department of Engineering, University of Leicester

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.

Concurrency First (but we'd better get it right!)
Peter H. WELCH, School of Computing, University of Kent

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!

Engineering Emergence: an occam-pi Adventure
Peter H. WELCH (a), Kurt WALLNAU (b) and Mark KLEIN (b)
(a) School of Computing, University of Kent
(b) Software Engineering Institute, Carnegie Mellon University

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).