BibTeX Proceedings details

BibTex html text dump of PaperDB database.

PaperDB is GPL Software, see: http://paperdb.sourceforge.net.

@InProceedings{Roebbers09,
  title = "{CPA} {S}urvival {G}uide",
  author= "Roebbers, Herman",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Broadfoot09,
  title = "{A}n {O}verview of {ASD} - {F}ormal {M}ethods in {D}aily {U}se",
  author= "Broadfoot, Guy",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Sampson09,
  title = "occam on the {A}rduino",
  author= "Sampson, Adam T. and Jadud, Matthew C. and Jacobsen, Christian L.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{OguzBroenink09,
  title = "{U}se of {F}ormal {M}odels in {M}odel-driven {D}esign of {E}mbedded software",
  author= "Oguz, Oguzcan and Broenink, Jan F.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
}
@InProceedings{Welch09a,
  title = "{C}oncurrency {F}irst (but we'd better get it right!)",
  author= "Welch, Peter H.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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!"
}
@InProceedings{SampsonBrown09,
  title = "{C}locks",
  author= "Sampson, Adam T. and Brown, Neil C.C.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Brown09b,
  title = "{T}races for {T}esting",
  author= "Brown, Neil C.C.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Mir09,
  title = "{A} {S}tudy {I}nto the {M}odelling and {A}nalysis of {R}eal-{T}ime {FPGA} {B}ased {S}ystems",
  author= "Mir, Irfan",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Slipper09,
  title = "{S}ystems {M}odelling and {I}ntegration",
  author= "Slipper, Dan",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Cole09,
  title = "{H}ardware/{S}oftware {C}o-{D}esign {L}anguage {D}evelopment, {A}n {E}ng{D} {I}ntroduction",
  author= "Cole, Alex",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{YalcinBroenink09,
  title = "{R}obust {R}obot {S}oftware using {P}rocess {O}rientation",
  author= "Yalcin, Cagri and Broenink, Jan F.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
}
@InProceedings{Goldsmith09,
  title = "{B}eyond {M}obility - {W}hat {N}ext {A}fter {CSP}/pi?",
  author= "Goldsmith, Michael",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "1--6",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Torshizi09,
  title = "{T}he {SCOOP} {C}oncurrency {M}odel in {J}ava-like {L}anguages",
  author= "Torshizi, Faraz and Ostroff, Jonathan S. and Paige, Richard F. and Chechik, Marsha",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "7--27",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{VanderMeulenPecheur09,
  title = "{C}ombining {P}artial {O}rder {R}eduction with {B}ounded {M}odel {C}hecking",
  author= "Vander Meulen, José and Pecheur, Charles",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "29--48",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Murakami09,
  title = "{O}n {C}ongruence {P}roperty of {S}cope {E}quivalence for {C}oncurrent {P}rograms with {H}igher-{O}rder {C}ommunication",
  author= "Murakami, Masaki",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "49--66",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Bezemer09,
  title = "{A}nalysing g{CSP} {M}odels {U}sing {R}untime and {M}odel {A}nalysis {A}lgorithms",
  author= "Bezemer, Maarten M. and Groothuis, Marcel A. and Broenink, Jan F.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "67--88",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{BrownSmith09,
  title = "{R}elating and {V}isualising {CSP}, {VCR} and {S}tructural {T}races",
  author= "Brown, Neil C.C. and Smith, Marc L.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "89--103",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Klomp09,
  title = "{D}esigning a {M}athematically {V}erified {I}2{C} {D}evice {D}river using {ASD}",
  author= "Klomp, Arjen and Roebbers, Herman and Derwig, Ruud and Bouwmeester, Leon",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "105--116",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Barnes09,
  title = "{M}obile {E}scape {A}nalysis for occam-pi",
  author= "Barnes, Frederick R. M.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "117--134",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{TeigVannebo09,
  title = "{N}ew {ALT} for {A}pplication {T}imers and {S}ynchronisation {P}oint {S}cheduling",
  author= "Teig, Øyvind and Vannebo, Per Johan",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "135--144",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Ritson09,
  title = "{T}ranslating {ETC} to {LLVM} {A}ssembly",
  author= "Ritson, Carl G.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "145--158",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{PedersenKauke09,
  title = "{R}esumable {J}ava {B}ytecode - {P}rocess {M}obility for {P}rocess{J} targeting the {JVM}",
  author= "Pedersen, Jan Bækgaard and Kauke, Brian",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "159--172",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Sputh09,
  title = "{O}pen{C}om{RTOS}: {A} {R}untime {E}nvironment for {I}nteracting {E}ntities",
  author= "Sputh, Bernhard H.C. and Faust, Oliver and Verhulst, Eric and Mezhuyev, Vitaliy",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "173--184",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Martin09,
  title = "{E}conomics of {C}loud {C}omputing: a {S}tatistical {G}enetics {C}ase {S}tudy",
  author= "Martin, Jeremy M. R. and Barrett, Steven J. and Thornber, Simon J. and Bacanu, Silviu-Alin and Dunlap, Dale and Weston, Steve",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "185--195",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Clayton09,
  title = "{A}n {A}pplication of {C}o{SM}o{S} {D}esign {M}ethods to {P}edestrian {S}imulation",
  author= "Clayton, Sarah and Urquhart, Neil and Kerridge, Jon",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "197--204",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{ChalmersKerridge09,
  title = "{A}n {I}nvestigation into {D}istributed {C}hannel {M}obility {S}upport for {C}ommunicating {P}rocess {A}rchitectures",
  author= "Chalmers, Kevin and Kerridge, Jon",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "205--223",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Brown09a,
  title = "{A}uto-{M}obiles: {O}ptimised {M}essage-{P}assing",
  author= "Brown, Neil C.C.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "225--238",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{BialkiewiczPeschanski09,
  title = "{A} {D}enotational {S}tudy of {M}obility",
  author= "Bialkiewicz, Joël-Alexis and Peschanski, Frederic",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "239--261",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Vinter09,
  title = "{P}y{CSP} {R}evisited",
  author= "Vinter, Brian and Bjørndalen, John Markus and Friborg, Rune Møllegard",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "263--276",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Friborg09,
  title = "{T}hree {U}nique {I}mplementations of {P}rocesses for {P}y{CSP}",
  author= "Friborg, Rune Møllegard and Bjørndalen, John Markus and Vinter, Brian",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "277--292",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Mount09,
  title = "{CSP} as a {D}omain-{S}pecific {L}anguage {E}mbedded in {P}ython and {J}ython",
  author= "Mount, Sarah and Hammoudeh, Mohammad and Wilson, Sam and Newman, Robert",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "293--309",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{TristramBradshaw09,
  title = "{H}ydra: {A} {P}ython {F}ramework for {P}arallel {C}omputing",
  author= "Tristram, Waide B. and Bradshaw, Karen",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "311--324",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Lowe09,
  title = "{E}xtending {CSP} with {T}ests for {A}vailability",
  author= "Lowe, Gavin",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "325--347",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{KorsgaardHendseth09,
  title = "{D}esign {P}atterns for {C}ommunicating {S}ystems with {D}eadline {P}ropagation",
  author= "Korsgaard, Martin and Hendseth, Sverre",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "349--361",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Kosek09,
  title = "{JCSP} {A}gents-{B}ased {S}ervice {D}iscovery for {P}ervasive {C}omputing",
  author= "Kosek, Anna and Kerridge, Jon and Syed, Aly and Armitage, Alistair",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "363--373",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{SimpsonRitson09,
  title = "{T}oward {P}rocess {A}rchitectures for {B}ehavioural {R}obotics",
  author= "Simpson, Jonathan and Ritson, Carl G.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "375--386",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{GroothuisBroenink09,
  title = "{HW}/{SW} {D}esign {S}pace {E}xploration on the {P}roduction {C}ell {S}etup",
  author= "Groothuis, Marcel A. and Broenink, Jan F.",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "387--402",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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."
}
@InProceedings{Welch09b,
  title = "{E}ngineering {E}mergence: an occam-pi {A}dventure",
  author= "Welch, Peter H. and Wallnau, Kurt and Klein, Mark",
  editor= "Welch, Peter H. and Roebbers, Herman and Broenink, Jan F. and Barnes, Frederick R. M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, G. S. and Vinter, Brian",
  pages = "403--403",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn= "978-1-60750-065-0",
  year= "2009",
  month= "nov",
  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)."
}

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.