2.3 Process Algebras

The success on the application of formal methods to SA depends on the ability in finding models and formalisms adequate to this level of the development process. To this effect, process algebras are widely accepted for the specification of software systems, in particular for communication protocols and distributed systems. The systems so specified can be checked for equivalence, deadlock freedom, and other interesting properties.

In particular, we propose the use of the $\pi$-calculus [MPW92] for the specification of software architectures. The $\pi$-calculus is a simple and powerful process algebra which can express directly mobility [EN86], making easier the specification of dynamic systems. Mobility is achieved in the $\pi$-calculus by passing channel names as arguments of messages. Since the names received can be used as channels for future transmissions, this allows an easy and effective reconfiguration of the system.

The calculus permits the specification of both local and global choices . Local choices indicate that a process may decide, not depending on its context, to commit to a certain transition or not, and model nondeterministic behavior. Global choices indicate that a process only commits to a transition after an agreement with another process performing the complementary action (either by local or global choice), and model deterministic behavior. Thus, using the $\pi$-calculus, we are able to express whether a process can initiate a certain communication (and then it requires that its environment could follow its decisions), or it just offers a certain behavior to its environment.

The formal basis of the $\pi$-calculus permits the analysis of the specifications for bisimilarity, deadlock and other interesting properties, and also the development of automated verification tools [Vic94]. However, the $\pi$-calculus is a low level notation, which makes difficult its direct application to the specification of large systems. Hence, a higher level notation is required. Formal specifications in $\pi$-calculus can be incorporated into the description of components by extending one of the existing ADLs.