Skip Navigation

The Computer Journal 1996 39(4):303-324; doi:10.1093/comjnl/39.4.303
© 1996 by British Computer Society
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (1)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Barringer, H.
Right arrow Articles by Williams, A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

A Process Algebra Foundation for Reasoning about Core ELLA

H. Barringer1, G. Gouch1, B. Monahan2 * and A. Williams1 §

1 Department of Computer Science, University of Manchester, Manchester M13 9PL, UK, 2 Harlequin Ltd, Alderley Edge, UK

A process algebraic foundation has been developed for formal analysis of synchronous hardware designs represented through the commercially available hardware design language, ELLA. An underlying semantic foundation, based on input/output trace sets, is presented first through the use of state machines. Such a representation enables direct application of standard, fully automated trace equivalence checking tools. However, to overcome the computational limitations imposed by such analysis methods, the input/output trace semantics is represented through a synchronous process algebra, EPA. Primitive processes in EPA denote the behaviour of primitive hardware components, such as delays or multiplexers, with composition operators corresponding to the different ways in which behaviours may be built. Of particular significance is the parallel composition operator which captures the machinery for building networks from other components/networks. Actions in EPA are structured and signify the state of input and output signals. This structure, however, is abstracted by developing an algebra for the actions. In particular, parallel composition on processes neatly lifts to a special (synchronous) product operation on actions. The EPA representation forms a good basis for semi-automated high-level symbolic manipulation and reasoning tools. First, the original design structure can be maintained, thus easing the problems of user level feedback from tools. Secondly, the application of EPA to ELLA enables a deterministic finite automation form for EPA terms. This provides a route to tractable symbolic verification and simulation, using a state evolution method to establish strong bisimulation properties.

The method has been successfully applied to classes of unbounded state space systems.

Received November 11, 1994. revised May 7, 1996.

* Present address: Harlequin Ltd, Alderley Edge, UK. Email: howard{at}cs.man.ac.uk

§ Alan Williams acknowledges the additional financial support of DRA, Malvern, UK, and Harlequin Ltd, (Cambridge, UK).

Department of Computer Science, University of Manchester, Manchester M13 9PL, UK

{ddagger} The University of Manchester acknowledges support from the SERC via research grant GR/F 38174.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.