Mapeando CSP em UML-RT
AUTOR(ES)
Manoel Messias da Silva Menezes Junior
DATA DE PUBLICAÇÃO
2008
RESUMO
A integraÃÃo de mÃtodos formais com notaÃÃes semi-formais visuais à uma tendÃncia em engenharia de software. MÃtodos formais apresentam uma semÃntica precisa e permitem verificaÃÃo de propriedades. No entanto, nÃo sÃo considerados intuitivos. Por outro lado, notaÃÃes semi-formais visuais, como UML, sÃo facilmente integradas no processo de desenvolvimento de software. Assim, mÃtodos formais e semi-formais visuais sÃo complementares. CSP e UML-RT sÃo, respectivamente, exemplos de notaÃÃo formal e diagramÃtica usados para especificar e projetar sistemas concorrentes e distribuÃdos. CSP à um mÃtodo formal no qual processos representam unidades comportamentais que se comunicam atravÃs de canais de comunicaÃÃo, utilizando passagem de mensagem. UML-RT à uma extensÃo conservativa de UML na qual cÃpsulas sÃo unidades comportamentais que se comunicam atravÃs de portas de comunicaÃÃo. Portas realizam protocolos os quais especificam os sinais que podem ser enviados e recebidos atravÃs de uma porta, e a ordem na qual os sinais podem ser comunicados. Em um trabalho anterior, Ferreira apresentou um conjunto de regras que sistematizam o mapeamento de CSP para UML-RT, mas uma prova formal deste mapeamento nÃo foi apresentada. Assim, para garantir consistÃncia no desenvolvimento de sistemas concorrentes e distribuÃdos utilizando este mapeamento, a prova formal do mesmo à indispensÃvel, uma vez que nÃo faz sentido o esforÃo dedicado à especificaÃÃo do sistema em CSP e a verificaÃÃo de propriedades e refinamentos, se uma ou mais regras de mapeamento estiverem incorretas. No entanto, UMLRT nÃo possui uma semÃntica formal padrÃo. Entre outras propostas de semÃntica formal, Ramos propÃe uma semÃntica para UML-RT utilizando OhCircus (uma combinaÃÃo de CSP e Z com caracterÃsticas adicionais de orientaÃÃo a objetos) como modelo semÃntico. Neste trabalho, à proposta uma variaÃÃo da semÃntica de Ramos para UML-RT usando CSP como modelo semÃntico. Com base nesta semÃntica, à apresentada a prova do mapeamento de CSP para UML-RT, considerando o modelo de falhas e divergÃncias de CSP. Assim, este trabalho consolida a integraÃÃo de CSP e UML-RT proposta por Ferreira, no desenvolvimento de sistemas crÃticos, concorrentes e distribuÃdos. Um resultado interessante foi observar que, estritamente, as regras propostas por Ferreira nÃo preservam a semÃntica de CSP, essencialmente com relaÃÃo a aspectos de terminaÃÃo dos processos
ASSUNTO(S)
semi-formal methods regras de traduÃÃo uml-rt prova formal do mapeamento formal proof of the mapping formal methods translation rules mÃtodos semi-formais uml-rt ciencia da computacao csp csp mÃtodos formais
