db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%T HCSP: Imperative State and True Concurrency
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%A Adrian E. Lawrence
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X HCSP is an extension of CSPP which captures the semantics of
hardware compilation. Because it is a superset of CSPP, it
can describe both hardware and software and so is useful for
co\-design. The extensions beyond CSPP include: true
concurrency; new hardware constructors; and a simple and
natural way to represent imperative state. Both CSPP and
HCSP were invented to cope with problems that arose while
the author was trying to prove that the hardware that he had
designed correctly implemented channels between a processor
and an FPGA. Standard CSP did not capture priority, yet the
circuits in the FPGA and the occam processes in the
transputer both depended on priority for their correctness.
The attempt to extend CSP rigorously to handle such problems
of co\-design has led to develoments that seem to have a
much wider significance including a new way of unifying
theories for imperative programming. This paper reports on
the current state of HCSP and focuses on handling imperative
state and true concurrency. The acceptance denotational
semantics is described briefly.