DefiniÃao e implementacÃo do sistema de tipos da linguagem Circus

AUTOR(ES)
DATA DE PUBLICAÇÃO

2006

RESUMO

A busca constante pelo desenvolvimento de sistemas de software com qualidade vem despertando o interesse das grandes empresas na aplicaÃÃo de tÃcnicas formais. Dentre as linguagens formais, existem aquelas prÃprias para a modelagem de dados complexos, tal como Z, e outras prÃprias para a modelagem de comunicaÃÃo e concorrÃncia, tal como CSP. Circus à uma linguagem de especificaÃÃo, projeto e programaÃÃo que combina Z e CSP. AlÃm de possibilitar a especificaÃÃo de aspectos de dados e comportamentais de sistema concorrentes, Circus inclui um cÃlculo de refinamentos. Este à seu diferencial em relaÃÃo a outras integraÃÃes de Z com uma Ãlgebra de processos. Circus vem despertando interesse no meio industrial, manifestado atravÃs de colaboraÃÃes cientÃficas e tecnolÃgicas, e possui uma equipe envolvida na construÃÃo de ferramentas que visam facilitar sua utilizaÃÃo. Muitas destas ferramentas precisam de um verificador de tipos para prover mais garantias quanto a consistÃncia das especificaÃÃes e programas, e, conseqÃentemente, de seus resultados. Neste trabalho, apresentamos uma definiÃÃo formal para o sistema de tipos de Circus, com o intuito de auxiliar o desenvolvimento de um verificador de tipos para a linguagem. Optamos por primeiramente definir as regras de tipos de Circus para depois implementar o software que automatiza a aplicaÃÃo dessas regras. Esta decisÃo de projeto contribuiu para a construÃÃo robusta do verificador, pois a implementaÃÃo consiste em um mapeamento direto das regras de tipos para linhas de cÃdigo. TambÃm apresentamos a nossa estratÃgia de validaÃÃo do verificador atravÃs de elaboraÃÃo de testes de pequeno e grande porte, e integraÃÃes com outras ferramentas da linguagem: o JCircus, que à um tradutor de Circus para Java; e o CircusRefine, uma ferramenta de refinamentos que desenvolvemos especialmente para integrar o verificador de tipos. Ao definir o sistema de tipos de Circus, e disponibilizar um verificador de tipos, acreditamos que estamos dando uma importante contribuiÃÃo na evoluÃÃo de Circus, esclarecendo pontos essenciais de sua definiÃÃo como uma linguagem fortemente tipada e compatÃvel com Z e CSP, e estamos tambÃm contribuindo para o desenvolvimento de outras ferramentas da linguagem. Esperamos que o nosso trabalho possa servir de base para a definiÃÃo e implementaÃÃo dos sistemas de tipos das extensÃes de Circus

ASSUNTO(S)

ciencia da computacao mÃtodos formais formal languages modelagem de dados complexos concorrÃncia tools concurrenc formal methods sistemas de software

ACESSO AO ARTIGO

Documentos Relacionados