WoTUG - The place for concurrent processes

Programme and PDFs of Papers

Outline

The CPA 2004 programme comprises two full day, one half day, and two evening sessions. Each day will begin with a keynote talk. A late bar each evening and a conference dinner will provide ample opportunity to relax, socialize, and discuss issues informally.

The conference opens on Sunday evening with registration, an evening meal, and an informal evening session, only part of which will be in the bar. Monday morning will open with a welcome address by the Dean of the School of Technology at Oxford Brookes, Dr. Denise Morrey, and the first keynote talk. The conference will close after lunch on Wednesday.

Keynote speakers

A. W. Roscoe is Professor and Head of Department at Oxford University Computing Laboratory and Fellow of University College. He has long been a leader in CSP research and is author of the standard text: The Theory and Practice of Concurrency.

Dr. Michael Goldsmith is managing director of Formal Systems (Europe) Ltd, which continues to develop the successful FDR model-checking tool for CSP. He is also a Senior Research Fellow of Worcester College, Oxford.

Dr. Goldsmith and Prof. Roscoe were part of the team that won the Queen's award for industry in 1990 for Technological Achievement for the development of formal methods in the specification and design of microprocessors.

Schedule

Sunday, 5th. September, 2004
 18:00-19:30  Registration Headington Hill Hall
 18:00-19:00  Dinner Headington Hill Hall
 19.30-21:30  First Evening Session   (and late Registration) DEM06
 21:30-22:30  Bar  Sports Hall
Monday, 6th. September, 2004
 08:00-09:00 Breakfast Student Refectory
 08:30-09:00 Registration DEM11
 09:00-09:10 Introduction and Welcome
Dr. Denise Morrey, Head of the School of Technology
DEM06
 09:10-10:00 First Keynote Talk
Finitary Refinement Checks for Infinitary Specifications
A. W. Roscoe
Professor and Head of Department at Oxford Computing Laboratory
DEM06
 10:00-10:30 Session 1: Communicating Process Architecture
Dynamic BSP: Towards a Flexible Approach to Parallel Computing over the Grid
Jeremy Martin and Alex Tiskin
DEM06
 10:30-11:00 Tea/Coffee DEM11
 11:00-12:30 Session 1 continued
K-CSP Component Based Development of Kernel Extensions
Bernhard Sputh and Alastair Allen
Chaining Communications Algorithms with CSP
Oliver Faust, Bernhard Sputh, David Endler, and Alastair Allen
Towards a Semantics for Prioritized Alternation
Ian East
DEM06
 13:00-14:00 Lunch (late registration in DEM11) DEM11
 14:00-15:30 Session 2: Formal derivation of systems
Refining Industrial Scale Systems in Circus
Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock
A Calculated Implementation of a Control System
Alistair A. McEwan
Derivation of Scalable Message-Passing Algorithms Using Parallel Combinatorial List Generator Functions
Ali Abdallah and John Hawkins
DEM06
 15:30-16:00 Tea/Coffee DEM11
 16:00-17:30 Session 3: Hardware derivation and verification
An Automatic Translation of CSP to Handel-C
Jonathan D. Phillips and G. S. Stiles
Using CSP to Verify Aspects of an Occam-to-FPGA Compiler
Roger Peel and Wong Han Feng Javier
Debugging and Verification of Parallel Systems - the picoChip Way
Daniel Towner, Gajinder Panesar, Andrew Duller, Alan Gray, and Will Robbins
DEM06
 17:30-18:00 WoTUG AGM DEM06
 18:00-19:00 Evening meal Research Centre SG01
 19.30-21:30  Second Evening Session DEM06
 21:30-23:00  Bar  Sports Hall
Tuesday 7th. September, 2004
 08:00-09:00 Breakfast Student Refectory
 09:10-10:00 Second Keynote Talk
CSP: The Best Concurrent-System Description Language in the World Probably!
Michael Goldsmith
Managing Director, Formal Systems Europe Ltd.
DEM06
 10:00-10:30 Session 4: Semantics and semantic models
Adrian E. Lawrence
Observing Processes
DEM06
 10:30-11:00 Tea/Coffee DEM11
 11:00-13:00 Session 4 continued
Triples
Adrian E. Lawrence
On Linear Time and Congruence in Channel-Passing Calculi
Frederic Peschanski
Focussing on Traces to Link VCR and CSP
Marc L. Smith
DEM06
 13:00-14:00 Lunch DEM11
 14:00-15:30 Session 5: Architecture, tools, and infrastructure
Prioritised Service Architecture
Ian East
Graphical Tool for Designing CSP Systems
Dusko S. Jovanovic, Geert K. Liet, and Jan F. Broenink
Active Serial Port: A Component for JCSPNet Embedded Systems
Sarah Clayton and Jon Kerridge
DEM06
 15:30-16:00 Tea/Coffee DEM11
 16:00-17:30 Session 6: Architecture, tools, and infrastructure cont.
C++CSP Networked
Neil Brown
Communicating Mobile Processes
Fred Barnes and Peter Welch
Adding Mobility to Networked Channel-Types
Mario Schweigler
DEM06
 17:30-18:00 Panel Session DEM06
 19:30-20:00 Reception Headington Hill Hall
 20:00-22:00 Conference Dinner Headington Hill Hall
 22:00-23:00  Bar  Sports Hall
Wednesday, 8th. September, 2004
 08:00-09:00 Breakfast Student Refectory
 09:00-10:30 Session 7: Hardware derivation and verification
Design of a Transputer Core and Implementation in an FPGA
Makoto Tanaka, Naoya Fukuchi, Yutaka Ooki, and Chikara Fukunaga
The Transterpreter: A Transputer Interpreter
Christian Jacobsen and Matthew C. Jadud
Reconfigurable Hardware Synthesis of the IDEA Cryptographic Algorithm
I. W. Damaj and Ali Abdallah
DEM06
 10:30-11:00 Tea/Coffee DEM13
 11:00-12:30 Session 8: Network implementation
A Comparison of Three MPI Implementations
Brian Vinter
An Evaluation of Inter-Switch Connections
Brian Vinter and Hans H. Happe
DEM06
 12:30-13:00 Prize giving and announcements DEM06
 13:00-14:00 Lunch DEM13
End of conference

Top of schedule

Proceedings

The contents list of the published proceedings of this conference are available here in PDF form.

The PDF versions of all of the papers are accessible from the links in the abstracts, below.

Top of schedule

Invited Papers

Finitary Refinement Checks for Infinitary Specifications
Prof. A. W. Roscoe, Professor and Head of Department, Computing Laboratory, Oxford University, UK

Abstract. We see how refinement against a variety of infinite-state CSP specifications can be translated into finitary refinement checks. Methods used include turning a process into its own specification inductively, and we recall Wolper's discovery that data independence can be used for this purpose.      PDF


CSP: The Best Concurrent-System Description Language in the World - Probably!
Dr. Michael Goldsmith, Managing Director, Formal Systems Europe Ltd., Oxford, UK

Abstract. CSP, Hoare's Communicating Sequential Processes}, is one of the formalisms that underpins the antecedents of CPA, and this year celebrates its Silver Jubilee. Formal Systems' own FDR refinement checker is among the most powerful explicit exhaustive finite-state exploration tools, and is tailored specifically to the CSP semantics. The CSPm ASCII form of CSP, in which FDR scripts are expressed, is the de-facto standard for CSP tools. Recent work has experimentally extended the notation to include a probabilistic choice construct, and added functionality into FDR to produce models suitable for analysis by the Birmingham University PRISM tool.      PDF


Top of schedule

Accepted Papers

Prioritised Service Architecture
Ian East, Dept. for Computing, Oxford Brookes University, UK

Abstract. Previously, Martin gave formal conditions under which a simple design rule guarantees deadlock-freedom in a system with service (client-server) architecture. Both conditions and design rule may be statically verified. Here, they are re-arranged to define service protocol, service network (system), and service network component, which together form a model for system abstraction. Adding mutual exclusion of service provision and dependency between service connections enriches abstraction and is shown to afford compositionality. Prioritised alternation of service provision further enriches abstraction while retaining deadlock-freedom and denying priority conflict, given appropriate new design rules.      PDF


Top of schedule

Towards a Semantics for Prioritized Alternation
Ian East, Dept. for Computing, Oxford Brookes University, UK

Abstract. A new prioritised alternation programming construct and CSP operator have previously been suggested by the author to express behaviour that arises with machine-level prioritised vectored interruption. The semantics of each is considered, though that of prioritisation is deferred given the current lack of consensus regarding a suitable domain. Defining axioms for the operator are tentatively proposed, along with possible laws regarding behaviour. Lastly, the issue of controlled termination of component and construct is explored. This is intended as only a first step towards a complete semantics.      PDF


Top of schedule

On Linear Time and Congruence in Channel-Passing Calculi
Frederic Peschanski, University of Tokyo, Japan

Abstract. Process algebras such as CSP or the Pi-calculus are theories to reason about concurrent software. The Pi-calculus also introduces channel passing to address specific issues in mobility. Despite their similarity, the languages expose salient divergences at the formal level. CSP is built upon trace semantics while labelled transition systems and bisimulation are the privileged tools to discuss the Pi-calculus semantics. In this paper, we try to bring closer both approaches at the theoretical level by showing that proper trace semantics can be built upon the Pi-calculus. Moreover, by introducing locations, we obtain the same discriminative power for both the trace and bisimulation equivalences, in the particular case of early semantics. In a second part, we propose to develop the semantics of a slightly modified language directly in terms of traces. This language retains the full expressive power of the Pi-calculus and most notably supports channel passing. Interestingly, the resulting equivalence, obtained from late semantics, exhibits a nice congruence property over process expressions.      PDF


Top of schedule

A Calculated Implementation of a Control System
Alistair A. McEwan, Computing Laboratory, University of Kent, UK

Abstract. In this paper, a case study consisting of a plant, and associated control laws, is presented. An abstract specification of the control system is given in Hoare's Communicating Sequential Processes (CSP). Via a series of calculated refinements, an implementation is developed, and translated into a simulation in a Java-based library for CSP, JCSP. Verification of the development process is performed using the model-checker for CSP, FDR. The result is a complete, verified implementation of the control system.      PDF


Top of schedule

Graphical Tool for Designing CSP Systems
Dusko S. Jovanovic, Geert K. Liet, and Jan F. Broenink, Drebbel Institute for Mechatronics and Control Engineering, University of Twente, The Netherlands

Abstract. For a broad acceptance of an engineering paradigm, a graphical notation and supporting design tool seem inevitable. This paper discusses certain issues of developing a design environment for building systems based on CSP. Some of the issues discussed depend specifically on the underlying theory of CSP, while a number of them are common for any graphical notation and supporting tools, such as provisions for complexity management and design overview.      PDF


Top of schedule

Dynamic BSP: Towards a Flexible Approach to Parallel Computing over the Grid
Jeremy Martin, Oxagen Ltd, Oxford, UK
Alexander Tiskin, Dept, of Computer Science, University of Warwick, UK

Abstract. The Bulk Synchronous model of parallel programming has proved to be a successful paradigm for developing portable, scalable, high performance software. Originally developed for use with traditional supercomputers, it was later applied to networks of workstations. Following the emergence of grid computing, new programming models are needed to exploit its potential. We consider the main issues relating to adapting BSP for this purpose, and propose a new model Dynamic BSP, which brings together many elements from previous work in order to deal with quality-of-service and heterogeneity issues. Our approach uses a task-farmed implementation of supersteps.      PDF


Top of schedule

K-CSP Component Based Development of Kernel Extensions
Bernhard Sputh and Alastair Allen, Dept. of Engineering, University of Aberdeen, UK

Abstract. Kernel extension development suffers from two problems. Firstly, there is little to no code reuse. This is caused by the fact that most kernel extensions are coded in the C programming language. This language only allows code reuse either by using `copy and paste' or by using libraries. Secondly, the poor separation of synchronisation and functionality code makes it difficult to change one without affecting the other. It is, therefore, difficult to use the synchronisation mechanisms correctly. The approach proposed in this paper tries to solve these problems by introducing a component based programming model for kernel extensions, and a system based on this proposal is implemented for the Linux kernel. The language used for the implementation is Objective-C, and as a synchronisation mechanism Communicating Sequential Processes is used. This model allows the functionality and synchronisation of a component to be developed separately. Furthermore, due to the use of Communicating Sequential Processes it is possible to verify the correctness of the synchronisation. An example given in this paper illustrates how easy it is to use the K-CSP environment for development.      PDF


Top of schedule

Chaining Communications Algorithms with CSP
Oliver Faust, Bernhard Sputh, David Endler, DSP Centre, Ngee Ann Polytechnic, Singapore
Alastair Allen, Dept. of Engineering, University of Aberdeen, UK

Abstract. Software Defined Radio (SDR) requires a reliable, fast and flexible method to chain parameterisable algorithms. Communicating Sequential Processes (CSP) is a design methodology, which offers exactly these properties. This paper explores the idea of using a Java implementation of CSP (JCSP) to model a flexible algorithm chain for Software Defined Radio. JCSP offers the opportunity to distribute algorithms on different processors in a multiprocessor environment, which gives a speed up and keeps the system flexible. If more processing power is required another processor can be added. In order to cope with the high data rate requirement of SDR, optimized data transfer schemes were developed. The goal was to increase the overall system efficiency by reducing the synchronisation overhead of a data transfer between two algorithms. To justify the use of CSP in SDR, a system incorporating CSP was compared with a conventional system, in single and multiprocessor environments.      PDF


Top of schedule

A Comparison of Three MPI Implementations
Brian Vinter, University of Southern Denmark, Denmark
John M. Bjorndalen, Otto J. Anshus, and Tore Larsen, University of Tromso, Norway

Abstract. Various implementations of MPI are becoming available as MPI is slowly emerging as the standard API for parallel programming on most platforms. The open source implementations LAM-MPI and MPICH are the most widely used, while commercial implementations are usually tied to special hardware platforms. This paper compares these two open-source MPI-implementations to one of the commercially available implementations, MESH-MPI from MESH-Technologies. We find that the commercial implementation is significantly faster than the open-source implementations, though LAM-MPI does come out on top in some benchmarks.      PDF


Top of schedule

An Evaluation of Inter-Switch Connections
Brian Vinter and Hans Henrik Happe, University of Southern Denmark, Denmark

Abstract. In very large clusters it is not possible to get Ethernet switches that are large enough to support the whole cluster, thus a configuration with multiple switches are needed.This work seeks to evaluate the interconnection strategies for a new 300+ CPU cluster at the University of Southern Denmark. The focal point is a very inexpensive switch from D-Link which unfortunately offers only 24 Gb ports. We investigate different inter-switch connections and their impact at application level.      PDF


Top of schedule

Observing Processes
Adrian Lawrence, Dept. of Computer Science, University of Loughborough, UK

Abstract. This paper discusses the sorts of observations of processes that are appropriate to capture priority. The standard denotational semantics for CSP are based around observations of traces and refusals. Choosing to record a little more detail allows extensions of CSP which describe some very general processes including those that include priority. A minimal set of observations yields a language and semantics remarkably close to the standard Failures-Divergences model of CSP which is described in a companion paper. A slightly richer set of observations yields a somewhat less abstract language.      PDF


Top of schedule

C++CSP Networked
Neil Brown, Qinetiq, Malvern, UK

Abstract. One year ago, the Kent C++CSP Library was presented at this conference. C++CSP is an implementation of CSP ideas in C++. After it was presented, C++CSP was released to the world at large under the Lesser GNU Public Licence. It had always been the author's intention to develop a network capability in the library. This paper details the development of a network capability for the library and the results of benchmarks, which are encouragingly fast.      PDF


Top of schedule

An Automatic Translation of CSP to Handel-C
Jonathan D. Phillips and G. S. Stiles, Utah State University, Logan, Utah, USA

Abstract. We present tools that convert a subset of CSP into Handel-C code. Handel-C is similar to the standard C programming language, and can be itself converted to produce files to program an FPGA. We thus now have a process that can directly generate hardware from a verified high-level description. The CSP to Handel-C translator makes use of the Lex and Yacc programming tools. The Handel-C code produced is functional, but not necessarily optimized for all situations. The translator has been tested using several CSP scripts of varying complexity. The functionality of the resulting Handel-C programs has been verified with simulations, and two scripts were further checked with successful implementations on an FPGA.      PDF


Top of schedule

Triples
Adrian Lawrence, Dept. of Computer Science, University of Loughborough, UK

Abstract. The most abstract form of acceptance semantics for a variant of CSPP is outlined. It encompasses processes which may involve priority, but covers a much wider class of systems including real time behaviour. It shares many of the features of the standard Failures-Divergences treatment: thus it is only a Complete Partial Order when the alphabet of events is finite.      PDF


Top of schedule

Active Serial Port: A Component for JCSPNet Embedded Systems
Sarah Clayton and Jon Kerridge, School of Computing, Napier University, Edinburgh, UK

Abstract. The javax.comm package provides basic low-level access between Java programs and external input-output devices, in particular, serial devices. Such communications are handled using event listener technology similar to that used in the AWT package. Using the implementation of active AWT components as a model we have constructed an active serial port (ASP), using javax.comm, that gives a channel interface that is more easily incorporated into a JCSPNet collection of processes. The ASP has been tested in a real-time embedded system used to collect data from infrared detectors used to monitor the movement of pedestrians. The collected data is transferred across an Ethernet from the serial port process to the data manipulation processes. The performance of the JCSPNet based system has been compared with that supplied by the manufacturer of the detector and we conclude by showing how a complete monitoring system could be constructed in a scalable manner.      PDF


Top of schedule

Debugging and Verification of Parallel Systems - the picoChip Way
Daniel Towner, Gajinder Panesar, Andrew Duller, Alan Gray, and Will Robbins, picoChip Designs Ltd., Bath, UK

Abstract. This paper describes the methods that have been developed for debugging and verifying systems using devices from the picoArray(TM) family. In order to increase the computational ability of these devices the hardware debugging support has been kept to a minimum and the methods and tools described take this into account. An example of how some of these methods have been used to produce an 802.16 system is given. The important features of the new PC102 device are outlined.      PDF


Top of schedule

Design of a Transputer Core and Implementation in an FPGA
Makoto Tanaka, Naoya Fukuchi, Yutaka Ooki, and Chikara FukunagaTokyo Metropolitan University, Japan

Abstract. We have made an IP (Intellectual Property) core for the T425 transputer. The same machine instructions as the transputer are executable in this IP core (we call it TPCORE). To create an IP code for the transputer has two aspects. On one hand, if we could succeed in building our own one and put it in an FPGA, we could apply it as a core processor in a distributed system. We also intend to put it in a VLSI chip. On the other hand, if we can extend our transputer development starting from a very conventional one to more sophisticated ones, as Inmos proceeded to the T9000, we will eventually find our technological breakthrough for the bottlenecks that the original transputer had, such as the restriction of the number of communication channels. It is important to have an IP core for the transputer. Although TPCORE uses the same register set with the same functionality as transputer and follows the same mechanisms for link communication between two processes and interrupt handling, the implementation must be very different from original transputer. We have extensively used the micro-code ROM to describe any states that TPCORE must take. Using this micro code ROM for the state transition description, we could implement TPCORE economically on FPGA space and achieve efficient performance.      PDF


Top of schedule

The Transterpreter: A Transputer Interpreter
Christian Jacobsen and Matthew C. JadudComputing Laboratory, University of Kent, UK

Abstract. We have written the Transterpreter, a virtual machine for executing the transputer instruction set. This interpreter is a small, portable, and extensible run-time, intended to be easily ported to handheld computers, mobile phones, and other embedded contexts. In striving for this level of portability, occam programs compiled to Transputer byte-code can currently be run on desktop computers, handhelds, and even the LEGO Mindstorms robotics kit.      PDF


Top of schedule

Adding Mobility to Networked Channel-Types
Mario SchweiglerComputing Laboratory, University of Kent, UK

Abstract. This paper reports the specification of a sound concept for the  mobility of network-channel-types in KROC.net. The syntax and semantics of KROC.net have also been modified in order to integrate it more seamlessly into the occam-pi language. These new features are currently in the process of being implemented. Recent developments in occam-pi and KROC (such as mobile processes and live / dead channel-type-ends) are described, together with their impact on KROC.net. This paper gives an overview of the recent developments in KROC.net, and presents its proposed final semantics, as well as the proposed interface between the KROC.net infrastructure and the KROC compiler.      PDF


Top of schedule

Communicating Mobile Processes
Fred Barnes and Peter Welch, Computing Laboratory, University of Kent, UK

Abstract. This paper presents a new model for mobile processes in occam-pi. A process, embedded anywhere in a dynamically evolving network, may suspend itself mid-execution, be safely disconnected from its local environment, moved (by communication along a channel), reconnected to a new environment and reactivated. Upon reactivation, the process resumes execution from the same state (i.e. data values and code positions) it held when it suspended. Its view of its environment is unchanged, since that is abstracted by its synchronisation (e.g. channels and barriers) interface and that remains constant. The environment behind that interface will (usually) be completely different. The mobile process itself may contain any number of levels of dynamic sub-network. This model is simpler and, in some ways, more powerful than our earlier proposal, which required a process to terminate before it could be moved. Its formal semantics and implementation, however, throw up extra challenges. We present details and performance of an initial implementation.      PDF


Top of schedule

Refining Industrial Scale Systems in Circus
Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock, Computing Laboratory, University of Kent, UK

Abstract. Circus is a new notation that may be used to specify both data and behaviour aspects of a system, and has an associated refinement calculus. Although a few case studies are already available in the literature, the industrial fire control system presented in this paper is, as far as we know, the largest case study on the Circus refinement strategy. We describe the refinement and present some new laws that were needed. Our case study makes extensive use of mutual recursion; a simplified notation for specifying such systems and proving their refinements is proposed here.      PDF


Top of schedule

Reconfigurable Hardware Synthesis of the IDEA Cryptographic Algorithm
I. W. Damaj and Ali Abdallah, Centre for Applied Formal Methods, London South Bank University, UK

Abstract. The paper focuses on the synthesis of a highly parallel reconfigurable hardware implementation for the International Data Encryption Algorithm (IDEA). Currently, IDEA is well known to be a strong encryption algorithm. The use of such an algorithm within critical applications, such as military, requires efficient, highly reliable and correct hardware implementation. We will stress the affordability of such requirements by adopting a methodology that develops reconfigurable hardware circuits by following a transformational programming paradigm. The development starts from a formal functional specification stage. Then, by using function decomposition and provably correct data refinement techniques, powerful high-order functions are refined into parallel implementations described in Hoare's communicating sequential processes notation(CSP). The CSP descriptions are very closely associated with Handle-C hardware description language (HDL) program fragments. This description language is employed to target reconfigurable hardware as the final stage in the development. The targeted system in this case is the RC-1000 reconfigurable computer. In this paper different designs for the IDEA corresponding to different levels of parallelism are presented. Moreover, implementation, realization, and performance analysis and evaluation are included.      PDF


Top of schedule

Derivation of Scalable Message-Passing Algorithms Using Parallel Combinatorial List Generator Functions
Ali Abdallah and John Hawkins, Research Institute for Computing, London South Bank University, UK

Abstract. We present the transformational derivations of several efficient, scalable, message-passing parallel algorithms from clear functional specifications. The starting algorithms rely on some commonly used combinatorial list generator functions such as tails, inits, splits and cp (cartesian product) for generating useful intermediate results. This paper provides generic parallel algorithms for efficiently implementing a small library of useful combinatorial list generator functions. It also provides a framework for relating key higher order functions such as map, reduce, and scan with communicating processes with different configurations.
The parallelisation of many interesting functional algorithms can then be systematically synthesized by taking an off-the-shelf parallel implementation of the list generator and composing it with appropriate parallel implementations of instances of higher order functions. Efficiency in the final message-passing algorithms is achieved by exploiting data parallelism, for generating the intermediate results in parallel; and functional parallelism, for processing intermediate results in stages such that the output of one stage is simultaneously input to the next one. This approach is then illustrated with a number of case studies which include: testing whether all the elements of a given list are distinct, the maximum segment sum problem, the minimum distance of two sets of points, and rank sort. In each case we progress from a quadratic time initial functional specification of the problem to a linear time parallel message passing implementation which uses a linear number of communicating sequential processes. Bird-Meertens Formalism is used to concisely carry out the transformations.      PDF


Top of schedule

Using CSP to Verify Aspects of an Occam-to-FPGA Compiler
Roger Peel and Wong Han Feng Javier, Dept. of Computing, University of Surrey, UK

Abstract. This paper reports on the progress made in developing techniques for the verification of an occam to FPGA compiler.
The compiler converts occam programs into logic circuits that are suitable for loading into field-programmable gate arrays (FPGAs). Several levels of abstraction of these circuits provide links to conventional hardware implementations. Communicating Sequential Processes (CSP) has then been used to model these circuits. This CSP has been subjected to tests for deadlock and livelock freedom using the Failures-Divergence Refinement tool (FDR). In addition, FDR has been used to prove that the circuits emitted have behaviours equivalent to CSP specifications of the original occam source codes.      PDF


Top of schedule

Focussing on Traces to Link VCR and CSP
Marc Smith, Dept. of Computer Science, Colby College, Maine, USA

Abstract. View-Centric Reasoning (VCR) replaces CSP's perfect observer with multiple, possibly imperfect observers. To employ view-centric reasoning within existing CSP models requires a bookkeeping change. Specifically, VCR introduces parallel events as a new primitive for constructing traces, and distinguishes two types of event traces: histories and views. Previously, we gave the operational semantics of VCR, and demonstrated the utility of parallel event traces to reason for the first time unambiguously about the meaning of the Linda predicate operations rdp() and inp(). The choice of using an operational semantics to describe VCR makes direct comparison with CSP difficult; therefore, work is ongoing to recast VCR denotationally, then link it with the other CSP models within Hoare and He's Unifying Theories of Programming. Initial efforts in this direction led to a comparison of VCR with Lawrence's HCSP. In this paper, we present some recent insights and abstractions - inspired by modern quantum physics - that have emerged whilst contemplating parallel event traces in light of the unifying theories. These insights lead to a more natural expression of VCR traces, in the sense that they more closely resemble CSP traces, thus forming a basis for linking VCR and CSP.      PDF


Top of schedule


Page last modified on 2nd October 2004
Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org