Mapeamento UML-RT para p-calculus.

AUTOR(ES)
DATA DE PUBLICAÇÃO

2006

RESUMO

A UML (Unified Modeling Language) à uma linguagem de modelagem para especificar, construir e documentar artefatos de sistemas de software. A UML-RT, usada pela ferramenta Rational Rose RealTime (RoseRT), à uma extensÃo da UML que permite a modelagem de sistemas de tempo real distribuÃdos e guiados por evento. A UML-RT nÃo possui semÃntica formal, logo nÃo à possÃvel realizar verificaÃÃo formal do modelo. O presente trabalho propÃe o mapeamento dos elementos de comunicaÃÃo da UML-RT para a Ãlgebra de processos p-calculus, a fim de prover semÃntica formal à UML-RT. Com objetivo de automatizar o mapeamento, foi desenvolvido um protÃtipo de tradutor que captura o modelo UML-RT especificado na ferramenta RoseRT e determina suas definiÃÃes p-calculus. As definiÃÃes p-calculus geradas utilizam a sintaxe da gramÃtica do HAL-JACK, que à uma ferramenta integrada para verificaÃÃo e anÃlise de sistemas expressos em p-calculus, assim as definiÃÃes p-calculus podem ser submetidas ao HAL-JACK para verificaÃÃo formal de propriedades. Este trabalho detalha o mapeamento UML-RT para p-calculus, descreve o protÃtipo desenvolvido e apresenta alguns exemplos do mapeamento do modelo UML-RT para definiÃÃes p-calculus.

ASSUNTO(S)

Ãlgebra de processos verificaÃÃo formal pi-cÃlculo desenvolvimento de software semÃntica de linguagem de programaÃÃo programaÃÃo orientada para objetos uml modelagem (processos) operaÃÃo em tempo real

ACESSO AO ARTIGO

Documentos Relacionados