BibTeX Proceedings details

BibTex html text dump of PaperDB database.

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

@InProceedings{Roscoe04,
  title = "{F}initary {R}efinement {C}hecks for {I}nfinitary {S}pecifications",
  author= "Roscoe, A. W.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "1--18",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{PhillipsStiles04,
  title = "{A}n {A}utomatic {T}ranslation of {CSP} to {H}andel-{C}",
  author= "Phillips, Jonathan D. and Stiles, G. S.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "19--38",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{Peschansk04,
  title = "{O}n {L}inear {T}ime and {C}ongruence in {C}hannel-{P}assing {C}alculi",
  author= "Peschanski, Frederic",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "39--54",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{East04a,
  title = "{P}rioritised {S}ervice {A}rchitecture",
  author= "East, Ian R.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "55--70",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{DullerPanesar04,
  title = "{D}ebugging and {V}erification of {P}arallel {S}ystems - the pico{C}hip {W}ay",
  author= "Duller, Andrew and Panesar, Gajinder and Towner, Daniel",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "71--84",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{ClaytonKerridge04,
  title = "{A}ctive {S}erial {P}ort: {A} {C}omponent for {JCSPN}et {E}mbedded {S}ystems",
  author= "Clayton, Sarah and Kerridge, Jon",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "85--98",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{JacobsonJadud04,
  title = "{T}he {T}ransterpreter: {A} {T}ransputer {I}nterpreter",
  author= "Jacobsen, Christian L. and Jadud, Matthew C.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "99--106",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{Schweigle04,
  title = "{A}dding {M}obility to {N}etworked {C}hannel-{T}ypes",
  author= "Schweigler, Mario",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "107--126",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{VinterBj\orndalen04,
  title = "{A} {C}omparison of {T}hree {MPI} {I}mplementations",
  author= "Vinter, Brian and Bjørndalen, John Markus",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "127--136",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{HappeVinter04,
  title = "{A}n {E}valuation of {I}nter-{S}witch {C}onnections",
  author= "Happe, Hans Henrik and Vinter, Brian",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "137--146",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{Lawrence04a,
  title = "{O}bserving {P}rocesses",
  author= "Lawrence, Adrian E.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "147--156",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{Lawrence04b,
  title = "{T}riples",
  author= "Lawrence, Adrian E.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "157--184",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{Brown04,
  title = "{C}++{CSP} {N}etworked",
  author= "Brown, Neil C.C.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "185--200",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{BarnesWelch04,
  title = "{C}ommunicating {M}obile {P}rocesses",
  author= "Barnes, Frederick R. M. and Welch, Peter H.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "201--218",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{MartinTiskin04,
  title = "{D}ynamic {BSP}: {T}owards a {F}lexible {A}pproach to {P}arallel {C}omputing over the {G}rid",
  author= "Martin, Jeremy M. R. and Tiskin, Alex V.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "219--226",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{Goldsmith04,
  title = "{CSP}: {T}he {B}est {C}oncurrent-{S}ystem {D}escription {L}anguage in the {W}orld - {P}robably!",
  author= "Goldsmith, Michael",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "227--232",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{BroeninkJovanovic04,
  title = "{G}raphical {T}ool for {D}esigning {CSP} {S}ystems",
  author= "Broenink, Jan F. and Jovanovic, Dusko S.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "233--252",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{East04b,
  title = "{T}owards a {S}emantics for {P}rioritized {A}lternation",
  author= "East, Ian R.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "253--264",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{OliveiraCavalcant04,
  title = "{R}efining {I}ndustrial {S}cale {S}ystems in {C}ircus",
  author= "Oliveira, Marcel and Cavalcanti, Ana and Woodcock, Jim",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "281--310",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{Sputh04,
  title = "{K}-{CSP} {C}omponent {B}ased {D}evelopment of {K}ernel {E}xtensions",
  author= "Sputh, Bernhard H.C.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "311--324",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{FaustSputh04,
  title = "{C}haining {C}ommunications {A}lgorithms with {CSP}",
  author= "Faust, Oliver and Sputh, Bernhard H.C. and Endler, David",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "325--338",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{PeelJavier04,
  title = "{U}sing {CSP} to {V}erify {A}spects of an {O}ccam-to-{FPGA} {C}ompiler",
  author= "Peel, Roger M. A. and Javier, Wong Han Feng",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "339--352",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{Smith04,
  title = "{F}ocussing on {T}races to {L}ink {VCR} and {CSP}",
  author= "Smith, Marc L.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "353--360",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{TanakaFukuchi04,
  title = "{D}esign of a {T}ransputer {C}ore and {I}mplementation in an {FPGA}",
  author= "Tanaka, Makoto and Fukuchi, Naoya and Ooki, Yutaka and Fukunaga, Chikara",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "361--372",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}
@InProceedings{AbdallahDamaj04,
  title = "{R}econfigurable {H}ardware {S}ynthesis of the {IDEA} {C}ryptographic {A}lgorithm",
  author= "Abdallah, Ali E. and Damaj, I. W.",
  editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.",
  pages = "387--416",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004",
  isbn= "1 58603 458 8",
  year= "2004",
  month= "sep",
  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."
}

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.