Composing snippets

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. A central notion in our framework is the notion of a snippet. A snippet 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.