Composing Snippets

  • Igor Benko
  • Jo Ebergen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2549)


We introduce a simple formal framework for specifying and implementing concurrent systems. The framework enables the specification of safety and progress properties and is based on Enhanced Characteristic Functions. The use of Enhanced Characteristic Functions leads to simple definitions of operations such as hiding and various process compositions. We discuss two compositions: the network composition for building networks of processes and the specification composition for building specifications of processes. Ac entral notion in our framework is the notion of a snippet. Asn ippet represents a part behavior of a process satisfying one specific constraint. A specification of a concurrent process satisfying all constraints is expressed by means of a specification composition of snippets. We present various properties of the specification and network compositions that can be helpful in the specification and implementation of concurrent systems. We illustrate our design approach with the design of some asynchronous circuits.


Output Port State Graph Input Port Factorization Theorem Output Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Igor Benko. ECF Processes and Asynchronous Circuit Design. PhD thesis, University of Waterloo, Department of Computer Science, file, 1999. 4
  2. [2]
    Igor Benko and Jo Ebergen. Delay-insensitive solutions to the committee problem. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 228–237. IEEE Computer Society Press, November 1994. 2Google Scholar
  3. [3]
    Tomaso Bolognesi and Ed Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14:25–59, 1987. 2CrossRefGoogle Scholar
  4. [4]
    Janusz A. Brzozowski, Scott Hauck, and Carl-Johan H. Seger. Design of asynchronous circuits. In Brzozowski, J. A. and Seger, C.-J. H. Asynchronous Circuits, Chapter 15. Springer-Verlag, 1995. 2Google Scholar
  5. [5]
    M. E. Bush and M. B. Josephs. Some limitations to speed-independence in asynchronous circuits. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems. IEEE Computer Society Press, March 1996. 2Google Scholar
  6. [6]
    B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.Google Scholar
  7. [7]
    Al Davis and Steven M. Nowick. Asynchronous circuit design: Motivation, background, and methods. In Graham Birtwistle and Al Davis, editors, Asynchronous Digital Circuit Design, Workshops in Computing, pages 1–49. Springer-Verlag, 1995. 2Google Scholar
  8. [8]
    Edsger W. Dijkstra. Hierarchical ordering of sequential processes. Acta Informatica, 1:115–138, 1971. 28, 29, 31CrossRefMathSciNetGoogle Scholar
  9. [9]
    David L. Dill. Trace Theory for Automatic Hierachical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1989. 2Google Scholar
  10. [10]
    Jo C. Ebergen. AF ormal Approach to Designing Delay-Insensitive Circuits. Distributed Computing, 5(3):107–119, 1991. 2, 13, 14, 15zbMATHCrossRefGoogle Scholar
  11. [11]
    Jo C. Ebergen. Arbiters: an exercise in specifying and decomposing asynchronously communicating components. Science of Computer Programming, 18(3):223–245, June 1992. 2zbMATHCrossRefGoogle Scholar
  12. [12]
    W. C. Mallon, J. T. Udding, and T. Verhoeff. Analysis and applications of the XDI model. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 231–242, April 1999. 2, 7, 11, 18Google Scholar
  13. [13]
    Willem Mallon. Personal communication, 1997. 17Google Scholar
  14. [14]
    Radu Negulescu. Process Spaces and Formal Verification of Asynchronous Circuits. PhD thesis, Dept. of Computer Science, Univ. of Waterloo, Canada, August 1998. 2Google Scholar
  15. [15]
    Radu Negulescu and Ad Peeters. Verification of speed-dependences in single-rail handshake circuits. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 159–170, 1998. 2Google Scholar
  16. [16]
    Ivan E. Sutherland. Micropipelines. Communications of the ACM, 32(6):720–738, January 1989. 2CrossRefGoogle Scholar
  17. [17]
    Alan Turing. Lecture to the London Mathematical Society on 20 February 1947. In Charles Babbage Institute Reprint Series for the History of Computing, Vol. 10, 1986. MIT Press, 1947. 2Google Scholar
  18. [18]
    C. H. (Kees) van Berkel, Mark B. Josephs, and Steven M. Nowick. Scanning the technology: Applications of asynchronous circuits. Proceedings of the IEEE, 87(2):223–233, February 1999. 2Google Scholar
  19. [19]
    Jan L. A. van de Snepscheut. Trace Theory and VLSI Design. Springer-Verlag, Heidelberg, 1985. 2zbMATHGoogle Scholar
  20. [20]
    Tom Verhoeff. A Theory of Delay-Insensitive Systems. PhD thesis, Eindhoven University of Techology, 1994. 1, 2, 4, 7, 8, 9, 11, 13, 15, 18Google Scholar
  21. [21]
    Tom Verhoeff. Analyzing specifications for delay-insensitive circuits. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 172–183, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Igor Benko
    • 1
  • Jo Ebergen
    • 2
  1. 1.University of WaterlooWaterlooCanada
  2. 2.Sun Microsystems LaboratoriesPalo AltoUSA

Personalised recommendations