Detalhes bibliográficos
| Ano de defesa: |
2006 |
| Autor(a) principal: |
Juliana de Melo Bezerra |
| Orientador(a): |
Não Informado pela instituição |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Instituto Tecnológico de Aeronáutica
|
| Programa de Pós-Graduação: |
Não Informado pela instituição
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Não Informado pela instituição
|
| Palavras-chave em Português: |
|
| Link de acesso: |
http://www.bd.bibl.ita.br/tde_busca/arquivo.php?codArquivo=365
|
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. |
