| dc.description | 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 | |
