BibTeX Proceedings details

BibTex html text dump of PaperDB database.

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

@InProceedings{Sampson11a,
  title = "{T}his is a {P}arallel {P}arrot",
  author= "Sampson, Adam T.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
}
@InProceedings{Cook11,
  title = "{P}arallel {U}sage {C}hecking - an {O}bservation",
  author= "Cook, Barry M.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "One of the great strengths of CSP based concurrent
     programming languages (such as occam) is the support
     provided to the programmer in avoiding the creation of
     erroneous programs. One such support \–
     \textlessi\textgreaterparallel usage
     checking\textless/i\textgreater \– detects program
     behaviours that may leave a variable in an
     unpredictable state. Current implementations of this check
     are safe but can lead to inefficient program
     implementations. In some cases, a simple
     program transformation can be used to demonstrate the safety
     of programs that would otherwise fail existing tests. By
     presenting a simple (but generic) example, I will show that
     using such a transformation allows the creation of
     more efficient programs."
}
@InProceedings{Vella11,
  title = "{E}xploring {P}eer-to-{P}eer {V}irtualized {M}ultithreaded {S}ervices",
  author= "Vella, Kevin",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
}
@InProceedings{Ellis11,
  title = "{F}ormal {A}nalysis of {C}oncurrent {OS} ({RM}o{X}) {D}evice {D}rivers",
  author= "Ellis, Martin",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "Many tools exists for writing safe and correct device
     drivers for conventional operating systems, from runtime
     driver management layers (that try to detect errors and
     recover from them) to static analysis systems like
     SLAM. Unfortunately, these tools do not map well to the
     concurrent drivers we write for RMoX. This presentation
     will look at how we can build safe and correct device
     drivers, using traditional occam analysis approaches (such
     as CSP) and tools (such as FDR). Experiments in generating
     formal models of hardware/driver interfaces from our
     occam implementations will be described, along with how we
     intend to use these models to prove correctness properties
     for our drivers."
}
@InProceedings{Barnes11,
  title = "{G}uppy",
  author= "Barnes, Frederick R. M.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
}
@InProceedings{Sampson11b,
  title = "{D}istributing {C}oncurrent {S}imulation",
  author= "Sampson, Adam T.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
}
@InProceedings{Wilterdink11,
  title = "{D}emonstration of the {LUNA} {F}ramework",
  author= "Wilterdink, Robert J.W. and Bezemer, Maarten M. and Broenink, Jan F.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "--",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "In this demonstration of the LUNA hard real-time,
     multi-threaded, CSP-capable execution framework, we use the
     JIWY-II pan-tilt camera robotic setup. The webcam can rotate
     horizontally and vertically, driven by two electromotors,
     controlled by software written as LUNA concurrent processes.
     The loop control algorithms are designed and generated
     by 20-sim, a tool for modeling and designing (controlled)
     mechatronic systems. This way, all code is generated, i.e. a
     model-driven approach. The demo will show that the LUNA
     library is capable of controlling setups in hard real-time,
     and that the implemented real-time logger provides valuable
     insight in the applications behaviour, i.e.
     control algorithms and LUNA framework."
}
@InProceedings{Lowe11,
  title = "{I}mplementing {G}eneralised {A}lt",
  author= "Lowe, Gavin",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "1--34",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "In this paper we describe the design and implementation of
     a generalised alt operator for the Communicating Scala
     Objects library. The alt operator provides a choice between
     communications on different channels. Our generalisation
     removes previous restrictions on the use of alts that
     prevented both ends of a channel from being used in an
     alt. The cost of the generalisation is a much more difficult
     implementation, but one that still gives very acceptable
     performance. In order to support the design, and greatly
     increase our confidence in its correctness, we build CSP
     models corresponding to our design, and use the FDR model
     checker to analyse them."
}
@InProceedings{FriborgVinter11,
  title = "{V}erification of a {D}ynamic {C}hannel {M}odel using the {SPIN} {M}odel-{C}hecker",
  author= "Friborg, Rune Møllegard and Vinter, Brian",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "35--54",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "This paper presents the central elements of a new dynamic
     channel leading towards a flexible CSP design suited for
     high-level languages. This channel is separated into three
     models: a shared-memory channel, a distributed channel and a
     dynamic synchronisation layer. The models are described
     such that they may function as a basis for implementing a
     CSP library, though many of the common features known in
     available CSP libraries have been excluded from the models.
     The SPIN model checker has been used to check for the
     presence of deadlocks, livelocks, starvation, race
     conditions and correct channel communication behaviour. The
     three models are separately verified for a variety of
     different process configurations. This verification is
     performed automatically by doing an exhaustive verification
     of all possible transitions using SPIN. The joint result of
     the models is a single dynamic channel type which supports
     both local and distributed any-to-any communication. This
     model has not been verified and the large state-space may
     make it unsuited for exhaustive verification using a model
     checker. An implementation of the dynamic channel will be
     able to change the internal synchronisation mechanisms
     on-the-fly, depending on the number of channel-ends
     connected or their location."
}
@InProceedings{Skovhede11,
  title = "{P}rogramming the {CELL}-{BE} using {CSP}",
  author= "Skovhede, Kenneth and Larsen, Morten N. and Vinter, Brian",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "55--70",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "The current trend in processor design seems to focus on
     using multiple cores, similar to a cluster-on-a-chip model.
     These processors are generally fast and power efficient, but
     due to their highly parallel nature, they are notoriously
     difficult to program for most scientists. One such processor
     is the CELL broadband engine (CELL-BE) which is known for
     its high performance, but also for a complex programming
     model which makes it difficult to exploit the architecture
     to its full potential. To address this difficulty, this
     paper proposes to change the programming model to use the
     principles of CSP design, thus making it simpler to program
     the CELL-BE and avoid livelocks, deadlocks and race
     conditions. The CSP model described here comprises a thread
     library for the synergistic processing elements (SPEs) and a
     simple channel based communication interface. To examine the
     scalability of the implementation, experiments are performed
     with both scientific computational cores and synthetic
     workloads. The implemented CSP model has a simple API and is
     shown to scale well for problems with significant
     computational requirements."
}
@InProceedings{PedersenSowders11,
  title = "{S}tatic {S}coping and {N}ame {R}esolution for {M}obile {P}rocesses with {P}olymorphic {I}nterfaces",
  author= "Pedersen, Jan Bækgaard and Sowders, Matthew",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "71--85",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "In this paper we consider a refinement of the concept of
     mobile processes in a process oriented language. More
     specifically, we investigate the possibility of allowing
     resumption of suspended mobile processes with different
     interfaces. This is a refinement of the approach taken
     currently in languages like occam-\π. The goal of
     this research is to implement varying resumption interfaces
     in ProcessJ, a process oriented language being developed at
     UNLV."
}
@InProceedings{Warren11,
  title = "{P}rioritised {C}hoice over {M}ultiway {S}ynchronisation",
  author= "Warren, Douglas N.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "87--110",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "Previous algorithms for resolving choice over multiway
     synchronisations have been incompatible with the notion of
     priority. This paper discusses some of the problems
     resulting from this limitation and offers a subtle expansion
     of the definition of priority to make choice meaningful
     when multiway events are involved. Presented in this paper
     is a prototype extension to the JCSP library that enables
     prioritised choice over multiway synchronisations and which
     is compatible with existing JCSP Guards. Also discussed are
     some of the practical applications for this algorithm as
     well as its comparative performance."
}
@InProceedings{Cole11,
  title = "{A} {C}omparison {O}f {D}ata-{P}arallel {P}rogramming {S}ystems {W}ith {A}ccelerator",
  author= "Cole, Alex and McEwan, Alistair A. and Singh, Satnam",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "111--130",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "Data parallel programming provides an accessible model for
     exploiting the power of parallel computing elements without
     resorting to the explicit use of low level programming
     techniques based on locks, threads and monitors. The
     emergence of GPUs with hundreds or thousands of
     processing cores has made data parallel computing available
     to a wider class of programmers. GPUs can be used not only
     for accelerating the processing of computer graphics but
     also for general purpose data-parallel programming. Low
     level data-parallel programming languages based on the CUDA
     provide an approach for developing programs for GPUs but
     these languages require explicit creation and coordination
     of threads and careful data layout and movement. This
     has created a demand for higher level programming languages
     and libraries which raise the abstraction level of
     data-parallel programming and increase programmer
     productivity. The Accelerator system was developed by
     Microsoft for writing data parallel code in a high level
     manner which can execute on GPUs, multicore processors using
     SSE3 vector instructions and FPGA chips. This paper compares
     the performance and development effort of the high level
     Accelerator system against lower level systems which
     are more difficult to use but may yield better results.
     Specifically, we compare against the NVIDIA CUDA compiler
     and sequential C++ code considering both the level of
     abstraction in the implementation code and the execution
     models. We compare the performance of these systems using
     several case studies. For some classes of problems,
     Accelerator has a performance comparable to CUDA, but for
     others its performance is significantly reduced however in
     all cases it provides a model which is easier to use
     and allows for greater programmer productivity."
}
@InProceedings{Kerridge11,
  title = "{E}xperiments in {M}ulticore and {D}istributed {P}arallel {P}rocessing using {JCSP}",
  author= "Kerridge, Jon",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "131--142",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "It is currently very difficult to purchase any form of
     computer system be it, notebook, laptop, desktop server or
     high performance computing system that does not contain a
     multicore processor. Yet the designers of applications, in
     general, have very little experience and knowledge of how to
     exploit this capability. Recently, the Scottish Informatics
     and Computer Science Alliance (SICSA) issued a challenge to
     investigate the ability of developers to parallelise a
     simple Concordance algorithm. Ongoing work had also shown
     that the use of multicore processors for applications that
     have internal parallelism is not as straightforward as might
     be imagined. Two applications are considered: calculating pi
     using Monte Carlo methods and the SICSA Concordance
     application. The ease with which parallelism can be
     extracted from a single application using both single
     multicore processors and distributed networks of such
     multicore processors is investigated. It is shown that naive
     application of parallel programming techniques does not
     produce the desired results and that considerable care has
     to be taken if multicore systems are to result in improved
     performance. Meanwhile the use of distributed systems tends
     to produce more predictable and reasonable benefits
     resulting from parallelisation of applications."
}
@InProceedings{Kosek11,
  title = "{E}valuating {A}n {E}mergent {B}ehaviour {A}lgorithm for {E}nergy {C}onservation in {L}ighting {S}ystems {U}sing {JCSP}",
  author= "Kosek, Anna and Syed, Aly and Kerridge, Jon",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "143--156",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "Since the invention of the light bulb, artificial light is
     accompanying people all around the world every day and
     night. As the light bulb itself evolved a lot through years,
     light control systems are still switch-based and require
     users to make most of the decisions about its behaviour.
     This paper presents an algorithm for emergent behaviour in
     a lighting system to achieve stable, user defined light
     level, while saving energy. The algorithm employs a parallel
     design and was tested using JCSP."
}
@InProceedings{Bezemer11,
  title = "{LUNA}: {H}ard {R}eal-{T}ime, {M}ulti-{T}hreaded, {CSP}-{C}apable {E}xecution {F}ramework",
  author= "Bezemer, Maarten M. and Wilterdink, Robert J.W. and Broenink, Jan F.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "157--175",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "Modern embedded systems have multiple cores available. The
     CTC++ library is not able to make use of these cores, so a
     new framework is required to control the robotic setups in
     our lab. This paper first looks into the available
     frameworks and compares them to the requirements for
     controlling the setups. It concludes that none of
     the available frameworks meet the requirements, so a new
     framework is developed, called LUNA. The LUNA architecture
     is component based, resulting in a modular structure. The
     core components take care of the platform related issues.
     For each supported platform, these components have a
     different implementation, effectively providing a
     platform abstraction layer. High-level components take care
     of platform-independent tasks, using the core components.
     Execution engine components implement the algorithms taking
     care of the execution flow, like a CSP implementation. The
     paper describes some interesting architectural challenges
     encountered during the LUNA development and their solutions.
      It concludes with a comparison between LUNA, C++CSP2 and
     CTC++. LUNA is shown to be more efficient than CTC++ and
     C++CSP2 with respect to switching between threads. Also,
     running a benchmark using CSP constructs, shows that LUNA is
     more efficient compared to the other two. Furthermore, LUNA
     is also capable of controlling actual robotic setups with
     good timing properties."
}
@InProceedings{Jacobsen11,
  title = "{C}oncurrent {E}vent-driven {P}rogramming in occam-\π for the {A}rduino",
  author= "Jacobsen, Christian L. and Jadud, Matthew C. and Kilic, Omer and Sampson, Adam T.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "177--193",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "The success of the Arduino platform has made embedded
     programming widely accessible. The Arduino has seen many
     uses, for example in rapid prototyping, hobby projects, and
     in art installations. Arduino users are often not
     experienced embedded programmers however, and writing
     correct software for embedded devices can be challenging.
     This is especially true if the software needs to use
     interrupts in order to interface with attached devices.
     Insight and careful discipline are required to
     avoid introducing race hazards when using interrupt
     routines. Instead of programming the Arduino in C or C++ as
     is the custom, we propose using occam-\π as a language as
     that can help the user manage the concurrency introduced
     when using interrupts and help in the creation of
     modular, well-designed programs. This paper will introduce
     the Arduino, the software that enables us to run occam-\π
     on it, and a case study of an environmental sensor used in
     an Environmental Science course."
}
@InProceedings{HanlonHollis11,
  title = "{F}ast {D}istributed {P}rocess {C}reation with the {XMOS} {XS}1 {A}rchitecture",
  author= "Hanlon, James and Hollis, Simon J.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "195--207",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "The provision of mechanisms for processor allocation in
     current distributed parallel programming models is very
     limited. This makes difficult, or even prohibits, the
     expression of a large class of programs which require a
     run-time assessment of their required resources. This
     includes programs whose structure is irregular, composite or
     unbounded. Efficient allocation of processors requires
     a process creation mechanism able to initiate and terminate
     remote computations quickly. This paper presents the
     design, demonstration and analysis of an explicit mechanism
     to do this, implemented on the XMOS XS1 architecture, as a
     foundation for a more dynamic scheme. It shows that process
     creation can be made efficient so that it incurs only
     a fractional overhead of the total runtime and that it can
     be combined naturally with recursion to enable rapid
     distribution of computations over a system."
}
@InProceedings{Whitehead11,
  title = "{S}erving {W}eb {C}ontent with {D}ynamic {P}rocess {N}etworks in {G}o",
  author= "Whitehead, James",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "209--226",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "This paper introduces webpipes, a compositional web server
     toolkit written using the Go programming language as part of
     an investigation of concurrent software architectures. This
     toolkit utilizes an architecture where multiple functional
     components respond to requests, rather than the traditional
     monolithic web server model. We provide a classification of
     web server components and a set of type definitions based on
     these insights that make it easier for programmers to create
     new purpose-built components for their systems. The
     abstractions provided by our toolkit allow servers to be
     deployed using several concurrency strategies. We examine
     the overhead of such a framework, and discuss
     possible enhancements that may help to reduce this overhead."
}
@InProceedings{Chalmers11,
  title = "{P}erformance of the {D}istributed {CPA} {P}rotocol and {A}rchitecture on {T}raditional {N}etworks",
  author= "Chalmers, Kevin",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "227--242",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "Performance of communication mechanisms is very important in
     distributed systems frameworks, especially when the aim is
     to provide a particular type of behavior across a network.
     In this paper, performance measurements of the distributed
     Communicating Process Architectures networking protocol and
     stack is presented. The results presented show that for
     general communication, the distributed CPA architecture
     is close to the baseline network performance, although when
     dealing with parallel speedup for the Mandelbrot set, little
     performance is gained. A discussion into the future
     direction of the distributed CPA architecture and protocol
     in relation to occam-\π and other runtimes is also
     presented."
}
@InProceedings{Ritson11,
  title = "{O}bject {S}tore {B}ased {S}imulation {I}nterworking",
  author= "Ritson, Carl G. and Andrews, Paul S. and Sampson, Adam T.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "243--253",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "The CoSMoS project is building generic modelling tools and
     simulation techniques for complex systems. As part of this
     project a number of simulations have been developed in many
     programming languages. This paper describes a framework for
     interconnecting simulation components written in different
     programming languages. These simulation components are
     synchronised and coupled using a shared object space. This
     approach allows us to combine highly concurrent
     agent-based simulations written in occam-\π, with
     visualisation and analysis components written in flexible
     scripting languages such as Python and domain specific
     languages such as MATLAB."
}
@InProceedings{Huntbach11,
  title = "{A} {M}odel for {C}oncurrency {U}sing {S}ingle-{W}riter {S}ingle-{A}ssignment {V}ariables",
  author= "Huntbach, Matthew",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "255--272",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "This is a description of a model for concurrent computation
     based on single-writer single-assignment variables. The
     description is primarily graphical, resembling the
     interaction nets formalism. The model embodies rules in a
     process which may require two or more communications
     from other processes to respond. However, these are managed
     by a partial evaluation response on receiving a single
     communication."
}
@InProceedings{KorsgaardHendseth11,
  title = "{T}he {C}omputation {T}ime {P}rocess {M}odel",
  author= "Korsgaard, Martin and Hendseth, Sverre",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "273--286",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "In traditional real-time multiprocessor schedulability
     analysis it is required that all tasks are entirely serial.
     This implies that if a task is written in a parallel
     language such as occam, all parallelism in the task must be
     suppressed to enable schedulability analysis. Part of the
     reason for this restriction is the difficulty in analysing
     execution times of programs with a complex parallel
     structure. In this paper we introduce an abstract model for
     reasoning about the temporal properties of such programs.
     Within this model, we define what it means for a process to
     be easier to schedule than another, and the notion of
     upper bounds on execution times. Counterintuitive temporal
     behaviour is demonstrated to be inherent in all systems
     where processes are allowed an arbitrary parallel structure.
     For example, there exist processes that are guaranteed to
     complete on some schedule, that may not complete
     if executing less than the expected amount of computation.
     Not all processes exhibit such counterintuitive behaviour,
     and we identify a subset of processes that are well-behaved
     in this respect. The results from this paper is a necessary
     prerequisite for a complete schedulability analysis of
     systems with an arbitrary parallel structure."
}
@InProceedings{SaifhashemiBeerel11,
  title = "{S}ystem{V}erilog{CSP}: {M}odeling {D}igital {A}synchronous {C}ircuits {U}sing {S}ystem{V}erilog {I}nterfaces",
  author= "Saifhashemi, Arash and Beerel, Peter A.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "287--302",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "This paper describes how to model channel-based digital
     asynchronous circuits using SystemVerilog interfaces that
     implement CSP-like communication events. The interfaces
     enable explicit handshaking of channel wires as well as
     abstract CSP events. This enables abstract connections
     between modules that are described at different levels
     of abstraction facilitating both verification and design. We
     explain how to model one-to-one, one-to-many, one-to-any,
     any-to-one, and synchronized channels. Moreover, we describe
     how to split communication actions into multiple parts to
     more accurately model less concurrent handshaking protocols
     that are commonly found in many asynchronous pipelines."
}
@InProceedings{Posso11,
  title = "{P}rocess-{O}riented {S}ubsumption {A}rchitectures in {S}warm {R}obotic {S}ystems",
  author= "Posso, Jeremy C. and Sampson, Adam T. and Simpson, Jonathan and Timmis, Jon",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "303--316",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "Previous work has demonstrated the feasibility of using
     process-oriented programming to implement simple subsumption
     architectures for robot control. However, the utility and
     scalability of process-based subsumption architectures for
     more complex tasks and those involving multiple robots has
     not been proven. We report our experience of applying these
     techniques to the implementation of a standard
     foraging problem in swarm robotics, using occam-\π to
     implement a subsumption control system. Through building a
     system with a realistic level of complexity, we have
     discovered both advantages and disadvantages to
     the process-oriented subsumption approach for larger robot
     control systems."
}
@InProceedings{SlipperMcEwan11,
  title = "{A} {S}ystems {R}e-engineering {C}ase {S}tudy: {P}rogramming {R}obots with occam and {H}andel-{C}",
  author= "Slipper, Dan and McEwan, Alistair A.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "317--327",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "This paper introduces a case study exploring some of the
     legacy issues that may be faced when redeveloping a system.
     The case study is a robotics system programmed in occam and
     Handel-C, allowing us to draw comparisons between software
     and hardware implementations in terms of program
     architecture, ease of program code verification, and
     differences in the behaviour of the robot. The two languages
     used have been selected because of their model of
     concurrency and their relation to CSP. The case study
     contributes evidence that re-implementing a system from
     an abstract model may present implementation specific issues
     despite maintaining the same underlying program control
     structure. The paper identifies these problems and suggests
     a number of steps that could be taken to help mitigate some
     of the issues."
}
@InProceedings{Armstrong11,
  title = "{T}he {F}lying {G}ator: {T}owards {A}erial {R}obotics in occam-\π",
  author= "Armstrong, Ian and Pirrone-Brusse, Michael and Smith, A and Jadud, Matthew C.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "329--340",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "The Flying Gator is an unmanned aerial vehicle developed to
     support investigations regarding concurrent and parallel
     control for robotic and embedded systems. During ten weeks
     in the summer of 2010, we designed, built, and tested an
     airframe, control electronics, and a concurrent firmware
     capable of sustaining autonomous level flight. Ultimately,
     we hope to have a robust, open source control system capable
     of supporting interesting research questions exploring
     concurrency in real time systems as well as current issues
     in sustainable agriculture."
}
@InProceedings{Isobe11,
  title = "{CONPASU}-tool: {A} {C}oncurrent {P}rocess {A}nalysis {S}upport {T}ool based on {S}ymbolic {C}omputation",
  author= "Isobe, Yoshinao",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "341--362",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "This paper presents an analysis-method of concurrent
     processes with value-passing which may cause infinite-state
     systems. The method consists of two steps: sequentialisation
     and state-reduction. In the sequentialisation, the symbolic
     transition graph of a given concurrent process is derived by
     symbolic operational semantics. In the state-reduction, the
     number of states in the symbolic transition graph is reduced
     by removing needless internal transitions. Furthermore,
     this paper introduces an analysis-tool called CONPASU, which
     implements the analysis-method, and demonstrates how CONPASU
     can be used for automatically analyzing concurrent
     processes. For example, it can extract abstract behaviors,
     which are useful for understanding complex behaviors, by
     focusing on some interesting events."
}
@InProceedings{Yamakawa11,
  title = "{D}evelopment of an {ML} based {V}erification {T}ool for {T}imed {CSP} {P}rocesses",
  author= "Yamakawa, Takeshi and Ohashi, Tsuneki and Fukunaga, Chikara",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "363--375",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "We report the development of a verification tool for Timed
     CSP processes. The tool has been built on the functional
     programming language ML. The tool interprets processes
     described in both timed and untimed CSP, converting them to
     ML functions, and executing those functions for the
     verification of refinement in the timed traces and timewise
     traces models. Using the programmability of higher
     order functionality, the description of CSP processes with
     ML has been synthesised naturally. The effectiveness of the
     tool is demonstrated with an example analysing
     implementations of Fischer's algorithm for the exclusive
     control of a shared resource in a multi-processor
     environment."
}
@InProceedings{BonniciWelch11,
  title = "{M}obile {P}rocesses and {C}all {C}hannels with {V}ariant {I}nterfaces (a {D}uality)",
  author= "Bonnici, Eric and Welch, Peter H.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "377--377",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "The current model of mobile processes in occam-\π
     implements a
     \textlessem\textgreatersingle\textless/em\textgreater interface
     for host processes to use. However, different hosts holding
     different kinds of resource will naturally require different
     interfaces to interact with their visitors. So, current
     occam-\π mobiles have to offer a single union of all the
     interfaces needed and hosts must provide dummy arguments for
     those irrelevant to its particular calls. This opens the
     possibilty of programming errors in both hosts and mobile
     should those dummies mistakenly be used. This talk considers
     a revised model for mobile processes that allows
     \textlessem\textgreatermany\textless/em\textgreater interfaces. The
     talk also proposes a concept of
     \textlessem\textgreatervariant call
     channels\textless/em\textgreater, that expands on a
     mechanism proposed for the occam3 language, and shows a
     simple duality between the revised mobile processes and
     mobile variant call channels. An implementation of mobile
     variant call channels, via source-code transformation to
     standard occam-\π mobile channel bundles, has been
     devised \– which gives an implementation route for the
     revised mobile process model and an operational
     semantics. If time, the ideas will be illustrated with a
     case study based on the Santa Claus problem, where the elves
     and reindeer are mobile processes."
}
@InProceedings{Welch11,
  title = "{A}dding {F}ormal {V}erification to occam-\π",
  author= "Welch, Peter H. and Pedersen, Jan Bækgaard and Barnes, Frederick R. M. and Ritson, Carl G. and Brown, Neil C.C.",
  editor= "Welch, Peter H. and Sampson, Adam T. and Pedersen, Jan Bækgaard and Kerridge, Jon and Broenink, Jan F. and Barnes, Frederick R. M.",
  pages = "379--379",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn= "978-1-60750-773-4",
  year= "2011",
  month= "jun",
  abstract= "This is a proposal for the formal verification of
     occam-\π programs to be managed entirely within
     occam-\π. The language is extended with qualifiers on
     types and processes (to indicate relevance for verification
     and/or execution) and assertions about refinement (including
     deadlock, livelock and determinism). The compiler abstracts
     a set of CSPm equations and assertions, delegates their
     analysis to the FDR2 model checker and reports back in terms
     related to the occam-\π source. The rules for mapping the
     extended occam-\π to CSPm are given. The full range of
     CSPm assertions is accessible, with no knowledge of CSP
     formalism required by the occam-\π programmer. Programs
     are proved just by
     \textlessem\textgreaterwriting\textless/em\textgreater and
     \textlessem\textgreatercompiling\textless/em\textgreater
     programs. A case-study analysing a new (and elegant)
     solution to the
     \textlessem\textgreaterDining Philosophers\textless/em\textgreater
     problem is presented. Deadlock-freedom for colleges with
     \textlessem\textgreaterany\textless/em\textgreater number of
     philosphers is established by verifying an induction
     argument (the base and induction steps). Finally, following
     guidelines laid down by Roscoe, the careful use
     of \textlessem\textgreatermodel
     compression\textless/em\textgreater is demonstrated to
     verify directly the deadlock-freedom of an occam-\π
     college with 10\^{}2000 philosphers (in around 30
     seconds). All we need is a universe large enough to contain
     the computer on which to run it."
}

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.