WoTUG - The place for concurrent processes

Refer Proceedings details


%T Demonstration of the LUNA Framework
%A Robert J.W. Wilterdink, Maarten M. Bezemer, Jan F. Broenink
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Distributing Concurrent Simulation
%A Adam T. Sampson
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011


%T Guppy
%A Frederick R. M. Barnes
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011


%T Formal Analysis of Concurrent OS (RMoX) Device Drivers
%A Martin Ellis
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Exploring Peer\-to\-Peer Virtualized Multithreaded Services
%A Kevin Vella
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011


%T Parallel Usage Checking \- an Observation
%A Barry M. Cook
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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 –
   <i>parallel usage checking</i>
   &ndash; 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.


%T This is a Parallel Parrot
%A Adam T. Sampson
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011


%T Implementing Generalised Alt
%A Gavin Lowe
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Verification of a Dynamic Channel Model using the SPIN Model\-Checker
%A Rune Møllegard Friborg, Brian Vinter
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Programming the CELL\-BE using CSP
%A Kenneth Skovhede, Morten N. Larsen, Brian Vinter
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Static Scoping and Name Resolution for Mobile Processes with Polymorphic Interfaces
%A Jan Bækgaard Pedersen, Matthew Sowders
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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\-&pi;. The goal of
   this research is to implement varying resumption interfaces
   in ProcessJ, a process oriented language being developed at
   UNLV.


%T Prioritised Choice over Multiway Synchronisation
%A Douglas N. Warren
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T A Comparison Of Data\-Parallel Programming Systems With Accelerator
%A Alex Cole, Alistair A. McEwan, Satnam Singh
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Experiments in Multicore and Distributed Parallel Processing using JCSP
%A Jon Kerridge
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Evaluating An Emergent Behaviour Algorithm for Energy Conservation in Lighting Systems Using JCSP
%A Anna Kosek, Aly Syed, Jon Kerridge
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T LUNA: Hard Real\-Time, Multi\-Threaded, CSP\-Capable Execution Framework
%A Maarten M. Bezemer, Robert J.W. Wilterdink, Jan F. Broenink
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Concurrent Event\-driven Programming in occam\-&pi; for the Arduino
%A Christian L. Jacobsen, Matthew C. Jadud, Omer Kilic, Adam T. Sampson
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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\-&pi; 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\-&pi; on it, and a case study of
   an environmental sensor used in an Environmental Science
   course.


%T Fast Distributed Process Creation with the XMOS XS1 Architecture
%A James Hanlon, Simon J. Hollis
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Serving Web Content with Dynamic Process Networks in Go
%A James Whitehead
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Performance of the Distributed CPA Protocol and Architecture on Traditional Networks
%A Kevin Chalmers
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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\-&pi; and other runtimes is also
   presented.


%T Object Store Based Simulation Interworking
%A Carl G. Ritson, Paul S. Andrews, Adam T. Sampson
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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\-&pi;, with
   visualisation and analysis components written in flexible
   scripting languages such as Python and domain specific
   languages such as MATLAB.


%T A Model for Concurrency Using Single\-Writer Single\-Assignment Variables
%A Matthew Huntbach
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T The Computation Time Process Model
%A Martin Korsgaard, Sverre Hendseth
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T SystemVerilogCSP: Modeling Digital Asynchronous Circuits Using SystemVerilog Interfaces
%A Arash Saifhashemi, Peter A. Beerel
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Process\-Oriented Subsumption Architectures in Swarm Robotic Systems
%A Jeremy C. Posso, Adam T. Sampson, Jonathan Simpson, Jon Timmis
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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\-&pi; 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.


%T A Systems Re\-engineering Case Study: Programming Robots with occam and Handel\-C
%A Dan Slipper, Alistair A. McEwan
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T The Flying Gator: Towards Aerial Robotics in occam\-&pi;
%A Ian Armstrong, Michael Pirrone-Brusse, A Smith, Matthew C. Jadud
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T CONPASU\-tool: A Concurrent Process Analysis Support Tool based on Symbolic Computation
%A Yoshinao Isobe
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.


%T Development of an ML based Verification Tool for Timed CSP Processes
%A Takeshi Yamakawa, Tsuneki Ohashi, Chikara Fukunaga
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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\[rs]s algorithm for the exclusive
   control of a shared resource in a multi\-processor
   environment.


%T Mobile Processes and Call Channels with Variant Interfaces (a Duality)
%A Eric Bonnici, Peter H. Welch
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X The current model of mobile processes in occam\-&pi;
   implements a <em>single</em> 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\-&pi; 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
   <em>many</em> interfaces. The talk also proposes
   a concept of <em>variant call
   channels</em>, 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\-&pi;
   mobile channel bundles, has been devised &ndash; 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.


%T Adding Formal Verification to occam\-&pi;
%A Peter H. Welch, Jan Bækgaard Pedersen, Frederick R. M. Barnes, Carl G. Ritson, Neil C.C. Brown
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X This is a proposal for the formal verification of
   occam\-&pi; programs to be managed entirely within
   occam\-&pi;. 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\-&pi; source. The rules for mapping
   the extended occam\-&pi; to CSPm are given. The full
   range of CSPm assertions is accessible, with no knowledge
   of CSP formalism required by the occam\-&pi; programmer.
    Programs are proved just by <em>writing</em>
   and <em>compiling</em> programs. A case\-study
   analysing a new (and elegant) solution to the
   <em>Dining Philosophers</em> problem is
   presented. Deadlock\-freedom for colleges with
   <em>any</em> 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 <em>model
   compression</em> is demonstrated to verify directly
   the deadlock\-freedom of an occam\-&pi; 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.

Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org

Valid HTML 4.01!