Web-based analysis of Reo connectors

Abstract

Combining independent software components usually requires additional code which can be difficult to maintain and is prone to errors. Connectors are used to describe how to combine independent components by restricting the possible interactions between their interfaces. The main focus of this work is on the formal analysis of Reo connectors, and a calculus of Reo connectors. The literature related to the formal analysis of Reo connectors provides different perspectives on it, which sometimes do not fit with each other on every level. The first part of this document presents the Reo connectors, accompanied by background work related to port automata semantics and an mCRL2 encoding of connectors. The remaining documented work focuses on the calculus of Reo connectors for which there are no tools to automatically analyse this calculus, other than a type-checker for an embedded domain specific language. We formalize this calculus in terms of port automata semantics, and provide an encoding, based on this semantics, to mCRL2. We also show that the formalized semantics, and the mCRL2 encoding are correct. Finally, we present a set of web-based tools for analysing connectors-named ReoLive-requiring only an offline Internet browser with JavaScript support, which also supports a client-server architecture for more complex operations. ReoLive includes tools that generate port automata, mCRL2 processes, and graphical representations of instances of connectors, developed in the Scala language and compiled into JavaScript. The resulting framework is publicly available, and can be easily experimented without any installation or a running server.

Combinar componentes de software independentes requer geralmente código adicional, que pode ser difícil de manter e facilmente conduz a erros. Conetores são usados para descrever a combinação de componentes independentes, através de restrições nas possíveis interações entre as suas interfaces. O principal foco deste trabalho encontra-se na análise formal de conetores Reo, e num cálculo de conetores Reo. A literatura relacionada com a análise formal de conetores Reo providencia perspetivas diferentes sobre esta, que, por vezes, não se encaixam perfeitamente entre si. A primeira parte deste documento apresenta os conetores Reo, e completa esta apresentação com algum trabalho anterior relacionado com a semântica em autómatos de porta e codificação de conetores em mCRL2. O restante trabalho documentado centra-se no cálculo de conetores Reo, para o qual não existem atualmente ferramentas para analisar automaticamente, para além de um type-checker para uma linguagem específica de conetores. Neste documento formalizamos o cálculo em termos de semântica de autómatos de porta, e definimos uma codificação, baseada nesta semântica, em mCRL2. Para além disso, mostramos que a semântica e a codificação estão corretos. Por último, introduzimos um conjunto de ferramentas baseadas em web para analisar conetores - chamada ReoLive - que requer apenas um explorador de internet offline, que suporte JavaScript, e que também permite uma arquitetura de cliente-servidor para operações mais complexas. O ReoLive inclui ferramentas que geram autómatos de porta, processos mCRL2, e representações gráficas de instâncias de conetores, desenvolvidas na linguagem Scala e que compilam para JavaScript. A framework final está disponível publicamente e pode ser experimentada sem qualquer instação ou servidor ativo.