Process algebras and meta-algebras: theory and practice
Samuël Weber · 1996
Verifying that a computer system--hardware, software, or both, does what is intended continues to be a pressing problem. In order to verify the correctness of a system, one first has to describe unambiguously its desired behaviour. This task is called specification, and also has proven in practice to be very difficult. This thesis argues for a methodology of specification and verification in which one builds specialized languages, tuned to the particular problem. There are two parts to this work. In the first, the algorithm for a compiler which translates programs written in a language called into electronic circuit diagrams is proven correct. This involved making specialized specification languages to describe the behaviour of Joy programs and of circuits, and then comparing the two. The techniques used are generalizable, and demonstrate that such specialized languages are feasible. The second part of this work describes a meta-language, called Meta-$\pi$, in which specialized specification languages can be built. These languages are of the same variety as used in the Joy work, and also include a popular specification language called $\pi$-calculus. With the Meta-$\pi$ family of languages, one can construct a language which is tuned to describe a particular problem. Since various desirable properties are proven to hold for all Meta-$\pi$ languages, one is automatically able to use these properties without having to do the substantial amount of work that would otherwise be needed to verify them.