In formal specification languages for parallel processes, such as CSP and LOTOS, algebraic laws for basic operators are provided that can be used to transform process expressions, and in particular, composition of processes can be calculated using these laws. Process composition can be used to simplify and improve the specification, and also to prove properties of the specification such as deadlock absence. We here test the practicality of process composition using CSP and suggest useful techniques, working in an example with nontrivial size and complexity. We emphasize that the size explosion of composed processes, caused by interleaving of the events of component processes, is a serious problem. Then we propose a technique, which we name two-way pipe, that can be used to reduce the size of the composed process, regarded as a program optimization at specification level.

A specification formalism for business application software is presented. Our approach is to investigate specification documents which are actually used in development projects of business applications in banking, insurance, and government systems. Since the specification documents are prepared mainly for users' review for the developing software, the representation of the documents is designed to be easy to understand for users, only in business terminology without losing a certain level of formality. Also, to avoid redundancy of the specification, there are some implicit assumptions in the specification. We have analyzed some commonality of these assumptions hidden in specification documents and are trying to construct a language by formalizing the underlying system model.