Essa linha de pesquisa tem como objetivo investigar os métodos existentes de especificação formal de sistemas distribuídos e de sistemas concorrentes para uma possível adequação às necessidades do BCG. Esse estudo poderá levar à definição de um novo formalismo.
A necessidade da utilização de técnicas de especificação formal para sistemas distribuídos deve-se principalmente à complexidade inerente a esse tipo de sistema. A utilização de descrições informais pode levar a descrições imprecisas e inconsistentes. É sabido que diferentes interpretações de uma mesma especificação podem levar facilmente à implementações incompatíveis, uma conseqüência desastrosa, principalmente quando se trata de sistemas onde cada serviço é realizado de forma distribuída.
Desse modo, os métodos de especificação formal permitem o desenvolvimento de sistemas sem ambigüidades, através de uma sintaxe e semântica bem definidas.