| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 1.82 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
A qualidade do Software foi sempre uma das grandes preocupações das empresas de desenvolvimento de software. O suporte à constante necessidade de actualização e adaptações dos sistemas é essencial ao sucesso dos mesmos.
O paradigma orientado a objectos centraliza uma grande parte dos seus esforços, na criação de sistemas de software bem planeados, robustos, modificáveis e, sempre que possível, reutilizáveis.
O UML (Unified Modelling Language) é uma linguagem de modulação visual, complementada pela linguagem de especificação formal de restrições OCL (Object Constraint Language). O OCL permite aumentar a expressividade dos diagramas, mas não consegue colmatar totalmente a informalidade do UML.
O refinamento baseia-se na premissa de que temos uma dada especificação e através de um conjunto de regras bem-formadas podemos obter uma segunda especificação aperfeiçoada, em que o comportamento inicialmente observado é mantido.
O Alloy é uma linguagem de especificação formal, orientada a objectos, direccionada para a criação de micro-modelos, que nos possibilita a análise e verificação formal, através da ferramenta associada Alloy Analyzer.
Com o objectivo de verificar a correcção das transformações de refinamento de diagramas de classe do UML, propomos a definição de um conjunto de regras de refinamento. Com base nessas regras e nos modelos (modelo original e concreto), propomos usar a ferramenta Alloy Analyzer para a verificação formal automática da correcção do refinamento.
Descrição
Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Engenharia Informática
Palavras-chave
Diagramas de classes UML (Unified Modelling Language) OCL (Object Constraint Language) Alloy e alloy analyzer Transformações de refinamento
