Exception handling sequential processes : design, verification and implementation

The design of an exception handling mechanism for communicating sequential processes is presented. It is primarily concerned with correctness of parallel programs using the mechanism. The proposed mechanism relies on only two basic additions to the notions already needed to cope with sequential program exceptions. To demonstrate that the exception handling mechanism serves the design of correct rubust parallel programs, a sound and relatively complete proof system is introduced for the enriched host programming language. Furthermore, the adequacy of the exception handling mechanism with the underlying programming model is shown. The programming language integrating the mechanism may be rewritten in terms of commands of the embedding language. Finally, comparison with related work is described