Formal contracts for derivation and verification of parallel componentes

The use of cloud computing to offer High Performance Computing (HPC) services has been widely discussed in the academia and industry. In this respect, this dissertation is included in the context of designing a cloud computing platform for the development of component-based parallel computing applications, referred as cloud of components. Many important challenges about using the cloud of components relate to parallel programming, an error-prone task due to synchronization issues, which may lead to abortion and production of incorrect data during execution of applications, and the inefficient use of computational resources. These problems may be very relevant in the case of long running applications with tight timelines to obtain critical results, quite common in the context of HPC. One possible solution to these problems is the formal analysis of the behavior of the components of an application through the cloud services, before their execution. Thus, the users of the components may know if a component can be safely used in their application. In this scenario, formal methods becomes useful. In this dissertation, it is proposed a process for specification and derivation of parallel components implementation for the cloud of components. This process involves the formal specification of the components behavior through contracts described using the Circus formal specification language. Then, through a refinement and translation process, which takes the contract as a start point, one may produce an implementation of a component that may execute on a parallel computing platform. Through this process, it becomes possible to offer guarantees to developers about the components behavior in their applications. To validate the proposed idea, the process is applied to contracts that have been described based on two benchmarks belonging to the NAS Parallel Benchmarks, widely adopted in HPC for evaluate the performance of parallel programming and computing platforms.A aplicação de nuvens computacionais para oferecer serviços de Computação de Alto Desempenho (CAD) é um assunto bastante discutido no meio acadêmico e industrial. Esta dissertação está inserida no contexto do projeto de uma nuvem computacional para o desenvolvimento e execução de aplicações de CAD baseadas em componentes paralelos, doravante denominada nuvem de componentes. Um dos principais desafios na sua utilização consiste no suporte à programação paralela, tarefa bastante suscetível à erros, pois tais erros podem levar, ao longo do desenvolvimento, a problemas de sincronização de processos, que podem causar abortamento da execução e a produção de dados incorretos, bem como a problemas relacionados ao uso ineficiente dos recursos computacionais. É importante que tais problemas sejam tratados no caso de aplicações de longa duração cujo respeito a um cronograma para obtenção de resultados é crítico, aplicações estas bastante comuns no contexto de CAD. Uma possível solução para tais problemas consiste na verificação do comportamento e das propriedades dos componentes na nuvem, antes que seja feita a sua execução, tornando possível que os usuários dos componentes da nuvem saibam se um componente pode ser utilizado com segurança em sua aplicação. Nesse cenário, o uso de métodos formais surge como uma alternativa atraente. A contribuição desta dissertação consiste em um processo de derivação e verificação de propriedades de componentes na nuvem. Tal processo envolve a especificação formal do comportamento dos componentes por meio de contratos descritos pela linguagem Circus. Então, através de um processo de refinamento e tradução tendo como ponto de partida o contrato, chega-se à implementação de um componente para execução sobre uma plataforma de computação paralela. Através desse processo, torna-se possível oferecer garantias aos desenvolvedores em relação ao comportamento dos componentes no contexto de suas aplicações. Para a prova de conceito, o processo é aplicado sobre a especificação "papel-e-caneta" de dois benchmarks do NAS Parallel Benchmarks, IS e CG, bastante difundidos na área de CAD