Embed Size (px)
Citation preview
PONTIFÍCIA UNIVERSIDADE CATÓLICA DE MINAS GERAIS
Programa de Pós-Graduação em Informática
UM ARCABOUÇO PARA VERIFICAÇÃO AUTOMÁTICA DEMODELOS UML
Flávio Gonçalves Fernandes
Belo Horizonte
2011
Flávio Gonçalves Fernandes
UM ARCABOUÇO PARA VERIFICAÇÃO AUTOMÁTICA DEMODELOS UML
Dissertação apresentada ao Programa de
Pós-Graduação em Informática como re-
quisito parcial para qualificação ao Grau de
Mestre em Informática pela Pontifícia Uni-
versidade Católica de Minas Gerais.
Orientador: Mark Alan Junho Song
Belo Horizonte
2011
FICHA CATALOGRÁFICA Elaborada pela Biblioteca da Pontifícia Universidade Católica de Minas Gerais
Fernandes, Flávio Gonçalves F363a Um arcabouço para verificação automática de modelos UML / Flávio
Gonçalves Fernandes. Belo Horizonte, 2011. 95f.: il.
Orientador: Mark Alan Junho Song Dissertação (Mestrado) – Pontifícia Universidade Católica de Minas Gerais.
Programa de Pós-Graduação em Informática.
1. UML (Computação). 2. Modelagem de dados. 3. Engenharia de software. I. Song, Mark Alan Junho. II. Pontifícia Universidade Católica de Minas Gerais. Programa de Pós-Graduação em Informática. III. Título.
CDU: 681.3.03
Flávio Gonçalves Fernandes
UM ARCABOUÇO PARA VERIFICAÇÃO AUTOMÁTICA DE MODELOSUML
Dissertação apresentada ao Programa dePós-Graduação em Informática como re-quisito parcial para qualificação ao Grau deMestre em Informática pela Pontifícia Uni-versidade Católica de Minas Gerais.
Mark Song (Orientador) – PUC Minas
Humberto Torres Marques Neto – PUC Minas
Adriano César Machado Pereira – CEFET-MG
Belo Horizonte, 15 de Dezembro de 2011.
A minha família, por sempre me apoiarem e estarem ao meu lado.
AGRADECIMENTOS
Agradeço especialmente, aos meus pais, Geraldo Fernandes e Sônia Maria Gonçalves
Fernandes, irmãos Alexandre Gonçalves Fernandes e Júnio Gonçalves Fernandes, e à minha
amada Soraia de Souza Reis pela compreensão, incentivo, apoio, carinho e amor.
À Deus pela vida e por iluminar o meu caminho.
Ao meu orientador Mark Alan Junho Song, por aceitar me guiar na realização desse
trabalho, pelos sábios ensinamentos, pela paciência, dedicação e confiança que foram essências
para que pudesse atingir meus objetivos.
Aos professores do Mestrado em Informática Humberto Torres, Luiz Zárate, Raquel
Mini e Henrique Cota pelos conhecimentos transmitidos. Aos funcionários da PUC Minas, em
especial a Giovana Silva por todo suporte e atenção.
Aos colegas do LCC/CENAPAD, em especial meu amigo Cesar Correia, pelo forneci-
mento dos dados que foram fundamentais para a execução deste trabalho.
À PUC Minas e a CAPES, pelo apoio a realização desta dissertação.
Aos amigos, familiares, colegas de mestrado e colegas de trabalho pelo incentivo, apoio
e por estarem sempre ao meu lado.
Ao Glorioso Clube Atlético Mineiro por toda emoção vivida durante todos os anos de
minha vida.
Muito obrigado a todos que contribuíram de alguma forma para a concretização deste
trabalho.
RESUMO
A Unified Modeling Language (UML) é uma linguagem de modelagem visual utilizada paraespecificar, visualizar, construir e documentar artefatos de um sistema. Apesar de possuir mui-tos recursos para a modelagem de sistemas, a UML não possui uma semântica formal, queé essencial para realizar verificações e validações. Com o intuito de realizar verificações emdiagramas da UML, descreve-se nesta dissertação um arcabouço para realizar a verificação au-tomática dos diagramas de atividade, estado e sequência da UML. O arcabouço proposto temcomo objetivo: (a) fornecer uma abordagem para realizar a tradução dos diagramas de ativi-dade, estado e sequência para linguagem formal de entrada do verificador formal NuSMV; (b)automatizar o processo de tradução dos diagramas para a linguagem formal; (c) fornecer umconjunto de validações pré-definidas que são utilizadas para verificar os diagramas. Adicional-mente, descreve-se o projeto e implementação de uma ferramenta que encapsula o arcabouçoproposto. Por fim, apresentam-se estudos de caso que visa demonstrar como essa abordagempode auxiliar na validação de diagramas da UML.
Palavras-chave: Unified Model Language, Métodos Formais, Verificação Simbólica de Mode-los, Lógica Temporal e Engenharia de Software.
ABSTRACT
The Unified Modeling Language (UML) is a visual modeling language used for specifying,visualizing, constructing, and documenting system artifacts. Despite having many features forsystem modeling, UML lacks a formal semantics, which is essential to conduct verifications andvalidations. In order to carry out checks on UML diagrams, this paper describes a frameworkto perform automatic checking of activity, state and sequence UML diagrams. The proposedframework aims to: (a) provide an approach to perform the translation of activity, state andsequence diagrams to the formal language input of the formal checker NuSMV; (b) automatethe translation process of the diagrams to the formal language; (c) provide a set of predefinedvalidations that are used to check the diagrams. Additionally, we describe the design and imple-mentation of a tool that encapsulates the proposed framework. Finally, we present case studiesthat aim to demonstrate how this approach can assist in the validation of UML diagrams.
Keywords: Unified Model Language, Model Checking, Symbolic Model Checking, TemporalLogic and Software Engineering
LISTA DE FIGURAS
FIGURA 1 Ilustração da origem da UML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
FIGURA 2 Classificação dos diagramas da UML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
FIGURA 3 Diagrama de estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
FIGURA 4 Diagrama de atividade . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
FIGURA 5 Transições . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
FIGURA 6 Ramificação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
FIGURA 7 Bifurcação e união . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
FIGURA 8 Diagrama de sequência . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
FIGURA 9 Modelo de um forno microondas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
FIGURA 10 Construção de BDD . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
FIGURA 11 Estados que obedecem a fórmulas CTL básicas . . . . . . . . . . . . . . . . . . . . 35
FIGURA 12 Metodologia formal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
FIGURA 13 Diagrama de estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
FIGURA 14 Diagrama de atividade . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
FIGURA 15 Objeto de decisão . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
FIGURA 16 Múltiplos objetos de decisão conectados . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
FIGURA 17 Conexão entre caminhos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
FIGURA 18 Transições paralelas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
FIGURA 19 Diagrama de sequência . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
FIGURA 20 Parelismo e condicional . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
FIGURA 21 A execução de uma atividade/mensagem/estado implica na execução de
outra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
FIGURA 22 A execução de uma atividade/mensagem/estado implica na não execu-
ção de outra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
FIGURA 23 A execução de uma atividade/mensagem/estado significa a possibilidade
da execução de outra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
FIGURA 24 A execução de uma atividade/mensagem/estado depende da prévia exe-
cução de outra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
FIGURA 25 É possível que uma determinada atividade/mensagem/estado não seja
executado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
FIGURA 26 Uma determinada atividade/mensagem/estado nunca é executado . . . 58
FIGURA 27 Arquitetura da ferramenta . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
FIGURA 28 Interface de tradução . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
FIGURA 29 Interface de verificação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
FIGURA 30 Diagrama escalonador . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
FIGURA 31 Diagrama exclusão de dados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
FIGURA 32 Escalonador: atividades em sequência . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
FIGURA 33 Mensagem de sucesso . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
FIGURA 34 Escalonador: objeto de decisão . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
FIGURA 35 Mensagem de contraexemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
FIGURA 36 Exclusão de dados: caminhos distintos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
FIGURA 37 Escalonador: paralelismo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
FIGURA 38 Exclusão de dados: antes e depois da remoção da transição de en-
trada . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
FIGURA 39 Diagrama emissão de nota fiscal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
FIGURA 40 Diagrama modos de operação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
FIGURA 41 Diagrama agendamento . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
FIGURA 42 Diagrama agendamento alterado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
FIGURA 43 Diagrama inserção de novo item . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
FIGURA 44 Inserção de novo item: paralelismo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
FIGURA 45 Inserção de novo item: condicional . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
FIGURA 46 Quadro de resultados dos testes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
LISTA DE QUADROS
QUADRO 1 Diagramas UML ........................................................................................... 21
QUADRO 2 Exemplo de um arquivo de entrada NuSMV ............................................. 36
QUADRO 3 Exemplo de uma instrução case ................................................................... 36
QUADRO 4 Exemplo de programa NuSMV com módulos reutilizáveis ...................... 39
QUADRO 5 Exemplo de programa NuSMV ................................................................... 39
QUADRO 6 Exemplo de programa NuSMV ................................................................... 40
QUADRO 7 Formalização do diagrama de estados ........................................................ 45
QUADRO 8 Diagrama de Estados .................................................................................... 46
QUADRO 9 Diagrama de Atividades - Declaração de variáveis ................................... 46
QUADRO 10 Diagrama de Atividades - Inicialização de variáveis ................................ 47
QUADRO 11 Transição Simples ........................................................................................ 47
QUADRO 12 Objeto de Decisão ........................................................................................ 48
QUADRO 13 Múltiplos Objetos de Decisão Conectados ................................................. 49
QUADRO 14 Conexão entre caminhos ............................................................................. 50
QUADRO 15 Transições Paralelas .................................................................................... 51
QUADRO 16 Diagrama de Sequência Simples - Declaração de variáveis ..................... 52
QUADRO 17 Inicialização das variáveis ........................................................................... 52
QUADRO 18 Transição simples ......................................................................................... 53
QUADRO 19 Condicional ................................................................................................... 53
QUADRO 20 Paralelismo ................................................................................................... 54
LISTA DE ABREVIATURAS E SIGLAS
BDD Bynari Decision Diagram
CTL Computation Tree Logic
CSP Communicating Sequential Processes
DTD Document Type Definition
IFES Instituições Federais de Ensino Superior
LCC Laboratório de Computação Científica
LTL Linear Temporal Logic
MEC Ministério da Educação
MOF Meta Objects Facility
OBDD Ordered Binary Decision Diagrams
OMG Object Management Group
OMT Object Modeling Technique
OOSE Object-Oriented Software Engineering
SESu Secretaria de Educação Superior
SMV Symbolic Model Verifier
UFMG Universidade Federal de Minas Gerais
UML Unified Modeling Language
V&V Verificação & Validação
XMI XML Metadata Interchange
XML Extensible Markup Language
W3C World Wide Web Consortium
SUMÁRIO
1 INTRODUÇÃO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.1 Motivação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.2 Objetivos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.3 Principais Contribuições . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.4 Estrutura da Dissertação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2 FUNDAMENTAÇÃO TEÓRICA. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1 Unified Modeling Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1.1 Visão Geral . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202.1.2 Diagrama de Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.1.3 Diagrama de Atividade . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.1.4 Diagrama de Sequência . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.1.5 XML Metadata Interchange . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.2 Verificação Simbólica de Modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.2.1 Estrutura Kripke . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.2 Diagrama Binário de Decisão . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.2.3 Lógica Temporal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.2.4 A Linguagem NuSMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
2.2.5 Módulo Main . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 362.2.6 Módulos Reutilizáveis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.2.7 Contraexemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3 TRABALHOS RELACIONADOS. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4 METODOLOGIA FORMAL PARAVERIFICAÇÃODEDIAGRAMASDAUML 44
4.1 Traduções . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.1.1 Tradução do Diagrama de Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.1.2 Tradução do Diagrama de Atividade . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.1.3 Tradução do Diagrama de Sequência . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.2 Verificações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.2.1 A execução de uma atividade/mensagem/estado implica na execução de outra . . 54
4.2.2 A execução de uma atividade/mensagem/estado implica na não execução deoutra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
4.2.3 A execução de uma atividade/mensagem/estado significa a possibilidade daexecução de outra. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
4.2.4 A execução de uma atividade/mensagem/estado depende da prévia execução deoutra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
4.2.5 É possível que uma determinada atividade/mensagem/estado não seja executado 57
4.2.6 Uma determinada atividade/mensagem/estado nunca é executado . . . . . . . . . . . . . 57
4.2.7 É sempre possível atingir o final do fluxo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.3 A Ferramenta para Automatização da Tradução e Verificação . . . . . . . . . . . . . . . . 58
5 ESTUDO DE CASO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 615.1 Unidades de Análise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 615.2 Validações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5.3 Avaliação e Resultados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5.3.1 Diagramas de Atividades . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5.3.2 Diagrama de Estados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
5.3.3 Diagrama de Sequência . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
5.3.4 Considerações Finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
6 CONCLUSÕES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 786.1 Trabalhos Futuros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
REFERÊNCIAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
ANEXO A -- DIAGRAMAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
ANEXO B -- LINGUAGEM SMV. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
15
1 INTRODUÇÃO
Modelos são representações gráficas que descrevem o problema e o sistema a serem
desenvolvidos. Devido às representações gráficas utilizadas, os modelos são frequentemente
mais compreensíveis do que as descrições detalhadas em linguagem natural dos requisitos de
sistema (SEIDEWITZ, 2003; LUDEWIG, 2003; LIEBERMAN, 2006; MULLER et al., 2010).
Os modelos podem ser utilizados no processo de análise para desenvolver uma compre-
ensão ou especificação do sistema requerido. Existem três diferentes perspectivas para repre-
sentar um sistema através de modelos (LUDEWIG, 2003; SOMMERVILLE, 2004; MULLER
et al., 2010) :
a) uma perspectiva externa, na qual o contexto ou o ambiente do sistema é modelado;
b) uma perspectiva de comportamento, no qual o comportamento do sistema e suas funcio-
nalidades são descritas;
c) uma perspectiva estrutural, em que a arquitetura ou a estrutura dos dados processados é
modelada.
No desenvolvimento de software, sistemas podem ser modelados através de diagramas,
que são descritos por uma linguagem de modelagem visual, como por exemplo Unified Mo-
deling Language (UML). Tal linguagem de modelagem visual (BOOCH; RUMBAUGH; JA-
COBSON, 2005) é de uso geral e pode ser utilizada para especificar, visualizar, construir e
documentar um sistema.
Devido às funcionalidades oferecidas, a UML apresenta vantagens inquestionáveis como
uma técnica de modelagem visual, e isso fez com que suas aplicações multiplicassem desde sua
criação em 1997. Com a explosão da utilização da UML, diversas ferramentas de apoio foram
desenvolvidas. Entretanto, inexiste a garantia de que os modelos gerados estejam corretos (FO-
WLER, 2003; PENDER, 2003; SEIDEWITZ, 2003; BOOCH; RUMBAUGH; JACOBSON,
2005).
1.1 Motivação
Erros humanos podem introduzir defeitos em qualquer etapa do ciclo de desenvolvi-
mento de software e, como consequência, o custo de se detectar e remover tais defeitos aumenta
16
consideravelmente através do ciclo de desenvolvimento de software (BASILI; PERRICONE,
1984; KANER; FALK; NGUYEN, 1999; FENTON; NEIL, 1999; OSTRAND; WEYUKER;
BELL, 2004; BELL; OSTRAND; WEYUKER, 2006). Ostrand, Weyuker e Bell (2005) citam
que ao se prevenir defeitos no início do desenvolvimento de software resulta em menor quanti-
dade de defeitos a serem encontrados nas fases posteriores. Portanto, pode-se inferir que a não
verificação dos modelos na etapa inicial influirá no custo de desenvolvimento de software, pois
os erros inseridos em modelos serão propagados às demais fases do ciclo de vida.
Pressman (2009) cita que uma modelagem sem erros traz importantes benefícios como
a possibilidade de se levantar a exatidão de uma implementação, ou seja, uma medida de con-
sistência entre a modelagem e o efeito do programa. Uma forma de se levantar essa exatidão é
através do processo de Verificação & Validação (V&V).
A V&V asseguram que o software desenvolvido cumpra com suas especificações e
atenda às necessidades. V&V constituem um processo de ciclo de vida completo, iniciando
com as revisões dos requisitos, lidando com as revisões de projeto e as inspeções de código até
se chegar aos testes de produto (SOMMERVILLE, 2004; SARGENT, 2007).
Inspeções e testes poderiam apoiar na verificação de modelos através de revisões dos
mesmos. Entretanto, verificar todas as combinações de entrada e pré-condições não é viável
exceto para casos triviais (OSTRAND; WEYUKER; BELL, 2005; GRAHAM et al., 2008;
FRASER; WOTAWA; AMMANN, 2009). A verificação de um sistema é trabalhosa e requer
ferramentas especializadas, como provadores de teoremas e técnicas de formalismo matemático
(CLARKE; LERDA, 2007; FRASER; WOTAWA; AMMANN, 2009).
Um exemplo de técnica baseada em formalismo matemático é o Método Formal. A
utilização de técnicas formais força uma análise detalhada das especificações, podendo reve-
lar inconsistências ou omissões em potencial que, de outro modo, permaneceriam sem serem
descobertas até que o sistema estivesse operacional (CLARKE; GRUMBERG; PELED, 1999;
SOMMERVILLE, 2004).
Os métodos formais capacitam o engenheiro de software a especificar, desenvolver e
verificar um sistema computadorizado ao aplicar uma notação matemática rigorosa. Usando
uma linguagem formal de especificação proporciona um meio para se especificar um sistema,
de maneira que os aspectos e consistência possam ser avaliados sistematicamente. Além disso,
remove a ambiguidade e estimula maior rigor nas primeiras fases do processo de engenharia de
software (CLARKE; LERDA, 2007; PRESSMAN, 2009).
Entre as técnicas contidas emMétodos formais está a Verificação Simbólica deModelos,
que é utilizada para verificar se um modelo de estado finito satisfaz certas propriedades. O
propósito da técnica é fornecer um esquema objetivo de avaliar expressões, buscando confirmar
17
afirmativas ou obter contraexemplos no caso de reprovações (MCMILLAN, 1993; CLARKE et
al., 1995; BIERE et al., 1999).
Entretanto, tais métodos, para serem acessíveis, somente são integrados à engenharia de
software se ferramentas automatizadas estiverem à disposição para auxiliar a especificação e
verificação. Ferramentas têm sido desenvolvidas para automatizar o processo de especificação
e verificação como, por exemplo, para linguagem Z, Verificação de Modelos, Communicating
Sequential Processes (CSP) e outros (PRESSMAN, 2009; FRASER; WOTAWA; AMMANN,
2009).
1.2 Objetivos
Tendo em vista a necessidade para se garantir qualidade dos modelos UML, esta disser-
tação tem como objetivo principal apresentar um arcabouço para realizar a verificação automá-
tica de modelos da UML através de métodos formais, especificamente a Verificação Simbólica
de Modelos. Sendo assim, o objetivo geral decompõe-se nos seguintes objetivos específicos:
a) Criar uma abordagem para realizar a tradução dos diagramas de atividade, estado e sequên-
cia da UML para a linguagem formal de entrada do verificador de modelos NuSMV. Dessa
forma, a abordagem fornece uma metodologia para a transformação de um conjunto de
definições dos diagramas citados em um modelo formal;
b) Automatizar o processo de tradução dos diagramas para a linguagem formal. A automa-
ção da metodologia de tradução permitirá ao engenheiro de software realizar a formali-
zação dos diagramas sem a necessidade de conhecer técnicas formais;
c) Fornecer um conjunto de validações pré-definidas, para que seja possível avaliar os dia-
gramas da UML, tais como, diagrama de atividades, estado e sequência;
d) Criar uma ferramenta que permita ao engenheiro de software visualizar e realizar verifi-
cações de forma rápida e prática;
e) Avaliar a abordagem proposta nesta dissertação. Para avaliação, foram feitos estudos de
casos com os diagramas UML demonstrando a utilização do arcabouço.
1.3 Principais Contribuições
A principal contribuição desse trabalho é prover um arcabouço para tradução dos diagra-
mas de atividade, estado e sequência da UML que poderá ser utilizada por pesquisadores para
serem integradas em sistemas de modelagem de diagramas da UML. Além disso, o arcabouço
18
de tradução poderá ser utilizado como modelo para a tradução dos demais diagramas da UML,
ou seja, poderá ser expandido provendo então um arcabouço mais completo.
Este trabalho também contribui com uma ferramenta que poderá ser utilizada por enge-
nheiros de software na validação dos diagramas construídos. Esta ferramenta poderá permitir a
atenuação do tempo e do custo no processo de desenvolvimento de software, uma vez que, ao
utilizarem a ferramenta, os engenheiros de software poderão descobrir problemas na modela-
gem do software que talvez só fossem detectados tardiamente no processo.
Por fim, este trabalho apresenta um estudo de caso envolvendo projetos que utilizam a
solução proposta, demonstrando os benefícios do uso deste tipo de arcabouço no desenvolvi-
mento de software.
Resalta-se que como resultado desse trabalho foram publicados os seguintes artigos:
Um arcabouço para verificação automática de modelos UML (FERNANDES; ALAN, 2011a)
e Verification of UML Behavioral Diagrams using Symbolic Model Checking (FERNANDES;
ALAN, 2011b).
1.4 Estrutura da Dissertação
O presente trabalho é composto por sete capítulos. No Capítulo 2, são fornecidos os
conceitos que proporcionam o embasamento teórico, referentes à UML e a Verificação Sim-
bólica de Modelos, necessários à compreensão desta dissertação. Em seguida, no Capítulo 3,
são descritos alguns trabalhos relacionados ao domínio do problema. Logo após, o Capítulo 4
apresenta a metodologia desenvolvida para realizar verificação dos digramas UML através de
métodos formais. Nesse capítulo também é apresentado como são realizadas as traduções dos
diagramas de atividade, estado e sequência para a linguagem formal e as verificações propostas
que compõem o arcabouço. O Capítulo 5 apresenta os estudos de casos para demonstrar o uso
do arcabouço desenvolvido tanto no quesito das traduções quanto nas verificações. Por fim, o
Capítulo 6 apresenta as considerações finais desta dissertação, destacando suas contribuições e
possíveis trabalhos futuros.
19
2 FUNDAMENTAÇÃO TEÓRICA
Neste Capítulo é apresentada a fundamentação que deu suporte teórico para a realização
do presente trabalho, como os conceitos referentes à UML e Verificação Simbólica de Modelos,
necessários à compreensão desta dissertação.
2.1 Unified Modeling Language
As linguagens de modelagem orientadas a objeto surgiram entre meados dos anos 70 e
final dos anos 80 como metodologia aplicada à análise e ao projeto de software. Porém pou-
cos métodos se destacaram como foi o caso dos métodos Booch Method proposto por Booch,
Object-Oriented Software Engineering (OOSE) proposto por Jacobson e Object Modeling Te-
chnique (OMT) proposto por Rumbaugh (FOWLER, 2003).
Em outubro de 1994 a UML foi oficialmente homologada pela Object Management
Group (OMG), após Rumbaugh se juntar a Booch na empresa Rational, com o objetivo de uni-
ficar os métodos Booch e o OMT, dando origem, em 1995, a versão 0.8 da UML que representa
o Método Unificado (FOWLER, 2003; SELIC, 2006).
Pouco tempo depois, Jacobson passou a integrar o projeto, que incorporou a metodologia
OOSE. Essa união deu origem à versão 0.9 da UML, lançada em 1996 (FOWLER, 2003;
SELIC, 2006). A Figura 1 ilustra a origem da UML.
Após lançamento da versão 0.9, um consórcio de empresas como a Digital Equipament
Corporation, Hewlet-Packard, iLogix, Intel, IBM, MCI Systemhouse, Microsoft, Oracle, Rati-
onal, Texas Instruments e Unisys passaram a contribuir para uma definição forte e completa
da UML. Esta colaboração conduziu à UML 1.0, uma linguagem de modelagem mais expres-
siva, poderosa e aplicável a um maior número de problemas decorrentes do clico de vida de
desenvolvimento de software (FOWLER, 2003; SELIC, 2006).
A versão 1.0 foi oferecida à OMG, para a padronização, em 1997, em resposta ao seu
pedido de elaboração de uma linguagem de modelagem padrão. Uma versão revisada da UML,
a 1.1, foi aprovada e adotada pela OMG no mesmo ano. Em 1998, foi liberada a versão 1.2 e
no mesmo ano a OMG homologou a versão 1.3 da UML (FOWLER, 2003; SELIC, 2006).
Em 2001 a OMG homologou a versão 1.4 da UML e em 2002 a versão 1.5, mas foi a
versão 2.0, lançada em 2003 que trouxe mais alterações à UML. Atualmente a UML encontra-se
na versão 2.3 (SELIC, 2006).
20
Figura 1: Ilustração da origem da UML
Fonte: Pender (2003)
2.1.1 Visão Geral
A UML é uma linguagem de modelagem visual de uso geral que é aplicada para a espe-
cificação, visualização, construção e documentação dos artefatos de software. Pode ser utilizada
com os principais métodos de orientação a objetos e componentes, além de possuir suporte a
qualquer domínio de aplicação e plataforma de implementação. Isso quer dizer que a UML
pode ser utilizada para modelagem de software, não importa qual a linguagem de programa-
ção utilizada na implementação, ou qual o processo de desenvolvimento adotado (BOOCH;
RUMBAUGH; JACOBSON, 2005; SELIC, 2006).
A partir da versão 2.0, a UML disponibiliza 13 diagramas que permitem a criação de
perfis particulares para um determinado sistema. O Quadro 1 descreve os diagramas (OBJECT
MANAGEMENT GROUP, 2010).
21
Quadro 1 - Diagramas UML
Classes Estrutura interna dos objetos do sistema.
Objetos Estrutura das instâncias das classes em tempo de execução.
Estrutura Composta Estrutura interna e colaborações.
Componentes Dependências entre componentes do sistema.
Implantação Arranjo físico dos sistemas e componentes nos computadores.
Pacotes Agrupamento lógico de classes e dependência entre grupos.
Atividade Computações, workflows, fluxos de objetos e de controle.
Caso de Uso Comportamento do sistema para o usuário externo.
Máquina de estados Possíveis estados de um objeto e suas transições.
Sequência Tempo e ordem das mensagens entre objetos durante uma interação.
Interação geral Visualização do fluxo de controle.
Tempo Dinâmica do tempo e mudança de estados.
Comunicação Objetos e relação dentro de uma interação.
Fonte: Booch, Rumbaugh e Jacobson (2005)
A utilização de diversos diagramas tem como objetivo fornecer múltiplas visões do sis-
tema que será modelado, tornando possível analisá-los sob diversos aspectos e permitir que cada
diagrama complemente o outro.
Cada diagrama analisa o sistema, ou parte dele, sob uma determinada óptica, enquanto
alguns dão ênfase à visão externa de forma mais geral, outros adicionam detalhes mais técnicos
ou características específicas do sistema ou de um processo qualquer, detalhando o tempo de
processos críticos e estruturas dos objetos. Conforme a Figura 2, os diagramas são classifica-
dos em estrutural e comportamental (FOWLER, 2003; BOOCH; RUMBAUGH; JACOBSON,
2005):
a) Diagramas Estruturais: tem como objetivo visualizar e documentar aspectos estáticos
do sistema. Os diagramas que pertencem à classificação estrutural são os diagramas de
classe, componentes, objetos, implantação, pacotes e estruturas compostas;
b) Diagramas Comportamentais: tem como objetivo visualizar e documentar aspectos di-
nâmicos do sistema. Os diagramas que pertencem à classificação comportamental são
os diagramas de sequência, comunicação, caso de uso, estado, atividade, temporização e
visão geral da interação.
Neste trabalho três diagramas comportamentais da UML fazem parte do arcabouço pro-
posto, são elas: estado, atividades e sequência. A seguir apresentam-se as características de
cada um destes diagramas.
22
Figura 2: Classificação dos diagramas da UML
Fonte: Fowler (2003)
2.1.2 Diagrama de Estado
O diagrama de estado especifica as sequências de estados pelas quais um objeto passa
durante seu tempo de vida em resposta a eventos, juntamente com suas respostas a esses even-
tos. Conforme ilustra a Figura 3, fazem parte do diagrama de estado os elementos: estado,
evento e transição. Um estado é uma condição ou situação na vida de um objeto durante a qual
ele satisfaz alguma condição, realiza alguma atividade ou aguarda um evento. Um evento é a
especificação de uma ocorrência significativa que tem uma localização no tempo e no espaço.
Uma transição é um relacionamento entre dois estados, indicando que um objeto no primeiro
estado realizara certas ações e entrara no segundo estado quando um evento especificado ocor-
rer e condições especificadas estão satisfeitas (FOWLER, 2003; PENDER, 2003; BOOCH;
RUMBAUGH; JACOBSON, 2005).
2.1.3 Diagrama de Atividade
O diagrama de atividade mostra o fluxo de uma atividade para outra. Uma atividade é
uma execução em andamento não atômica em uma máquina de estados. As atividades efetiva-
mente resultam em alguma ação, formada pelas computações executáveis atômicas que resultam
em uma mudança de estado do sistema ou o retorno de um valor. As ações abrangem a chamada
a outras operações, enviando um sinal, criando ou destruindo um objeto ou alguma computação
23
Figura 3: Diagrama de estado
Fonte: Booch, Rumbaugh e Jacobson (2005)
pura, como o cálculo de uma expressão (FOWLER, 2003; PENDER, 2003; BOOCH; RUM-
BAUGH; JACOBSON, 2005).
Pode-se observar na Figura 4 os componentes que fazem parte do diagrama de atividade:
a) Iniciação (Estado Inicial);
b) Atividades (Ações ou Nó de atividade);
c) Fluxos de controle;
d) Ramificação/Mesclar;
e) Bifurcação/União;
f) Conclusão (Estado Final).
Fluxos de controle
Quando a ação ou o nó de atividade está completo, o fluxo de controle passa imediata-
mente à próxima ação ou nó de atividade. O fluxo é especificado utilizando setas de fluxo para
mostrar o caminho de uma ação ou nó de atividade para o seguinte. É representado por uma
seta simples da ação predecessora para a sucessora, sem um rótulo de evento, conforme mostra
a Figura 5 (FOWLER, 2003; PENDER, 2003; BOOCH; RUMBAUGH; JACOBSON, 2005).
24
Figura 4: Diagrama de atividade
Fonte: Booch, Rumbaugh e Jacobson (2005)
Figura 5: Transições
Fonte: Booch, Rumbaugh e Jacobson (2005)
25
Ramificação
Assim como em fluxogramas, nos diagramas de atividades pode-se incluir uma ramifi-
cação, especificando caminhos alternativos, tomados com base em alguma expressão booleana.
Conforme mostra a Figura 6, uma ramificação é representada como um diamante. A ramificação
poderá ter uma transição de entrada e duas ou mais de saída. Em cada transição de entrada, é
colocada uma expressão booleana, avaliada somente após a entrada na ramificação (FOWLER,
2003; PENDER, 2003; BOOCH; RUMBAUGH; JACOBSON, 2005).
Figura 6: Ramificação
Fonte: Booch, Rumbaugh e Jacobson (2005)
Bifurcação e União
Na UML, a barra de sincronização é empregada para especificar a bifurcação e a união
desses fluxos paralelos de controle. A barra de sincronização é representada como uma linha
fina, horizontal ou vertical. Conforme mostra a Figura 7, uma bifurcação representa a divisão
de um mesmo fluxo de controle em dois ou mais fluxos de controle concorrentes. A bifurcação
poderá ter uma única transição de entrada e duas ou mais transições de saída, cada uma das
quais representa um fluxo de controle independente. As atividades de cada um desses fluxos são
executadas de forma concorrente (FOWLER, 2003; PENDER, 2003; BOOCH; RUMBAUGH;
JACOBSON, 2005).
Pode-se observar que uma união representa a sincronização de dois ou mais fluxos de
controle concorrentes. A união poderá ter duas ou mais transições de entrada e uma única
transição de saída. Na união, os fluxos concorrentes são sincronizados, significando que cada
um aguarda até que todos os fluxos de entrada tenham alcançado a união no ponto em que um
dos fluxos de controle prossegue abaixo da união (FOWLER, 2003; PENDER, 2003; BOOCH;
RUMBAUGH; JACOBSON, 2005).
26
Figura 7: Bifurcação e união
Fonte: Booch, Rumbaugh e Jacobson (2005)
2.1.4 Diagrama de Sequência
O diagrama de sequência dá ênfase à ordenação temporal das mensagens. Conforme
mostra a Figura 8, um diagrama de sequência é formado colocando-se primeiro os objetos que
participam da interação no nível superior do diagrama, ao longo do eixo X. Geralmente, o
objeto que inicia a interação é colocado à esquerda e objetos mais subordinados vão crescendo
à direita. As mensagens que esses objetos enviam e recebem são colocadas ao longo do eixo
Y, em ordem crescente de tempo, de cima para baixo. Isso proporciona uma clara indicação
visual do fluxo de controle ao longo do tempo (FOWLER, 2003; PENDER, 2003; BOOCH;
RUMBAUGH; JACOBSON, 2005).
O principal conteúdo em um diagrama de sequência é o conjunto de mensagens. Uma
mensagem é apresentada por uma seta de uma linha da vida para outra. A seta aponta para o
destinatário. As mensagens podem ser assíncrona ou síncrona. Se a mensagem é assíncrona, a
linha tem uma seta fina. Se a mensagem é síncrona, a linha tem uma seta triangular cheia.
Execução Condicional
A execução condicional é marcada com a tag alt. O corpo do operador de controle é
dividido em várias sub-regiões por linhas horizontais tracejadas. Cada sub-região representa
27
Figura 8: Diagrama de sequência
Fonte: Booch, Rumbaugh e Jacobson (2005)
um ramo de um condicional. Cada sub-região é tem uma condição de proteção. Se a condição
de proteção for verdadeira, a sub-região será executada (FOWLER, 2003; PENDER, 2003;
BOOCH; RUMBAUGH; JACOBSON, 2005).
Execução Paralela
A execução paralela é marcada com a tag par. O corpo do operador de controle é di-
vido em várias sub-regiões por linhas horizontais tracejadas. Cada sub-região representa uma
computação paralela. Quando o operador de controle entra, todas as sub-regiões são executa-
das paralelamente (FOWLER, 2003; PENDER, 2003; BOOCH; RUMBAUGH; JACOBSON,
2005).
2.1.5 XML Metadata Interchange
O XML Metadata Interchange (XMI) é um documento Extensible Markup Language
(XML) definido e mantido pela OMG. Foi criado para ser um mecanismo para a troca de in-
formações contidas em um modelo entre as várias ferramentas que suportam a UML. Algumas
importantes indústrias da área de desenvolvimento de software orientado a objetos, incluindo a
IBM e Unisys, propuseram um novo padrão que combina os benefícios do XML para definição,
validação e compartilhamento de documentos com os benefícios da UML (GROUP, 2011).
28
XML é um padrão aberto e consolidado da World Wide Web Consortium (W3C), defi-
nido como um formato de dados para troca de documentos estruturados na internet. O objetivo
do XMI é permitir a troca de objetos definidos pela OMG com UML e Meta Objects Faci-
lity (MOF), representando esses objetos como elementos e atributos XML referenciados com o
uso de identificadores (GROUP, 2011).
Antes da definição do XMI como formato padrão definido pela indústria, cada ferra-
menta tinha seu próprio formato proprietário.
O XMI também pode ser usado para produzir Document Type Definition (DTD) e Sche-
mas XML automaticamente a partir de modelos UML e MOF, oferecendo uma descrição XML
para esses artefatos (GROUP, 2011).
Para cada elemento de um modelo da linguagem UML padrão existe um mapeamento
possível na estrutura de dados criada no documento XMI, fato importante que permite que a
prova de conceito construída neste trabalho possa receber como entrada um modelo criado em
qualquer ferramenta de modelagem UML disponível no mercado que conte com a funcionali-
dade de exportação desse tipo de documento.
Nesta dissertação foi realizado o reconhecimento dos padrões de mapeamento dos di-
agramas de estado, atividade e sequência, dessa forma, sendo possível fazer a tradução dos
mesmos para a linguagem formal.
2.2 Verificação Simbólica de Modelos
A Verificação Simbólica de Modelos permite certificar propriedades que descrevem um
modelo. O modelo é analisado exaustivamente com o objetivo de determinar se o mesmo está
em conformidade com certas propriedades (CLARKE; GRUMBERG; PELED, 1999).
Considera-se o sistema modelado como um conjunto finito de estados e por relações
de transição entre os mesmos. A partir de um conjunto finito de propriedades associadas ao
modelo, é possível definir, para cada um dos estados, um subconjunto dessas propriedades que
são verdadeiras naquele estado.
Cada propriedade é uma proposição atômica. O conjunto destas proposições atômicas
define cada um dos estados, de forma que dois estados diferentes não podem obedecer a exata-
mente o mesmo conjunto de proposições atômicas.
Especificamente, o sistema é descrito por um grafo de transição de estado que representa
o modelo a ser verificado, enquanto as propriedades são descritas como fórmulas em uma lin-
guagem temporal. Cada vértice do grafo corresponde a um estado do sistema. A singularidade
de cada estado é definida pelos valores contidos em cada uma de suas variáveis. As arestas no
grafo equivalem a transições entre estados. O procedimento de verificação irá percorrer todos
29
os estados do modelo até se certificar de que o mesmo atende às propriedades definidas. Se
alguma propriedade não foi válida, um contraexemplo é retornado mostrando os estados onde a
propriedade não é satisfeita no modelo. Esse processo é realizado através de três etapas:
a) Especificar as propriedades que o sistema deverá ter para ser considerado correto;
b) Construir um modelo formal para representar o sistema. O modelo deve prover um nível
de abstração do sistema que seja capaz de capturar todas as propriedades essenciais à
verificação, e omitir detalhes que não afetem a correção dessas propriedades;
c) Executar o verificador de modelos para validar as propriedades especificadas no primeiro
passo sobre o modelo criado no segundo passo. Dessa forma, aplica-se o verificador para
testar se o modelo atende às propriedades desejadas. Caso todas as propriedades sejam
atendidas, então o modelo está correto. Caso o modelo não atenda a alguma propriedade,
então é retornado um contraexemplo mostrando o porquê da sua invalidade.
2.2.1 Estrutura Kripke
Uma estrutura Kripke é uma estrutura utilizada para representar o modelo, essa estrutura
consiste em um grafo onde os vértices representam os estados, as arestas, o conjunto de tran-
sições entre estados, e uma função determina, para cada estado, um conjunto de propriedades
que são verdadeiras (CLARKE; GRUMBERG; PELED, 1999).
Clarke e Lerda (2007) definem formalmente que uma estrutura Kripke sobre um con-
junto de proposições atômicas P= p0, ..., pn−1 é uma quádrupla M = (S,S0,R,λ ), tal que:
a) S é um conjunto finito de estados;
b) s0 ⊆ S é o conjunto de estados iniciais;
c) R⊆ SxS é a relação total da transição de estados - para cada s ∈ S, existe um s′ ∈ S tal que
(s,s′) ∈ R;
d) λ : S→ 2p é a função que rotula cada estado s ∈ S com os valores 0 ou 1 associados a
cada pi ∈ P. O valor associado é 1 caso pi seja verdadeira e 0 caso contrário.
Um caminho sobre a estruturaM a partir de um estado s0 é definido como uma sequência
infinita de estados σ = s0s1...sn tal que s0 ∈ S e R(si,si+1) seja definida para todo i ≥ 0. Uma
sequência de rótulos de σ é uma palavra infinita λ (s0)λ (s1)... sobre o alfabeto 0,1|p|.
Segundo a definição acima, cada proposição corresponde a um valor binário. Entretanto,
essa pode não ser a melhor forma de se representar um sistema. Por exemplo, considere a
30
avaliação de alunos de uma universidade em que a média de aproveitamento de notas de um
aluno seja a variável de interesse. Suponha três faixas distintas: uma média menor que 70% de
aproveitamento, outra entre 70% e 90%, e outra maior que 90%. Dessa forma, a média poderia
ser representada pela letra B (Baixa) para a primeira faixa, N (Normal) para a segunda e A
(Alta) para a última. Nesse caso, a variável associada à média não poderia mais ser considerada
uma proposição atômica, como definida acima, por possuir três estados possíveis.
Entretanto, a definição de estrutura Kripke não fica limitada por esse tipo de problema,
pois três novas proposições atômicas x, y e z podem ser definas baseadas nos três estados
descritos acima. Sendo assim, x será verdadeira quando a média do aluno estiver abaixo de
70% e falsa nas outras ocasiões, enquanto y será verdadeira se a média estiver entre 70% e 90%
e falsa nas outras ocasiões, enquanto z será verdadeira quando a média for acima de 90% e
falso, caso contrário. Modelando o sistema dessa forma é possível obedecer à definição acima.
Entretanto, a complexidade do modelo será maior.
Outro exemplo de um sistema de estado finito pode ser visto na Figura 9 que representa
os possíveis estados de um forno microondas (CLARKE; GRUMBERG; PELED, 1999).
Figura 9: Modelo de um forno microondas
Fonte: Clarke, Grumberg e Peled (1999)
Cada um dos estados pode ser identificado através de uma quadrupla (Start Close Heat
Error), onde Start representa se o forno está ligado, Close se a porta está fechada, Heat se
o forno está aquecido, e Error se ocorreu algum erro de funcionamento. Qualquer uma dessas
variáveis só pode assumir os valores 0 ou 1, em que, o símbolo (˜) em frente ao nome da variável
significa que ela possui o valor 0, e caso contrário a variável possui o valor 1.
Considere o estado 0 como estado inicial, em que, o forno esta com a porta fechada,
desligado, não aquecido, e sem erro de funcionamento. A transição de estado R(0,5) representa
31
o forno ligado com a porta aberta, o que significa que ocorreu um erro e o forno não pode
aquecer. Nesse caso, o usuário pode fechar a porta do forno, o que leva à transição de estado
R(5,6). A partir daqui, caso o usuário abra novamente a porta do forno, volta-se para o estado 5
através da transição R(6,5), ou desliga-se o forno indo para o estado 1 através da transição R(6,1).
O estado 1 indica que o forno estará preparado para ser ligado. Esse estado é alcançado
através das transições de estado R(0,1), em que a porta é fechada antes de o forno ser ligado, ou
R(6,1) descrita anteriormente. A próxima transição de estado R(1,2) indica que o forno foi ligado
e agora pode ser aquecido através da transição R(2,3), e continuar-se aquecendo, indo para o
estado 4 através da transição R(3,4).
No estado 4, o forno está desligado, aquecendo-se com a porta fechada, e não ocorre
nenhum erro. Aqui ele pode continuar aquecendo (transição de estados R(6,6)), terminar o
aquecimento com aporta fechada (transição de estados R(6,1)), ou voltar para o estado inicial
(transição de estados R(6,1)).
Levando-se em conta o cenário apresentado acima, pode-se definir os quatro elementos
da estrutura Kripke M = (S,S0,R,λ ) para este modelo que se segue:
a) S= {i|0≤ i≤ 9};
b) S0 = {0};
c) R= {(0,1),(0,5),(1,0),(1,2),(2,3),(3,4),(4,0),(4,1),(4,4),(5,6),(6,1),(6,5),;
d) λ (0) = (0,0,0,0),λ (1) = (0,1,0,0),λ (2) = (1,1,0,0),λ (3) = (1,1,1,0),
λ (4) = (0,1,1,0),λ (5) = (1,0,0,1),λ (6) = (1,1,0,1).
2.2.2 Diagrama Binário de Decisão
Bryant (1986) foi o responsável por formalizar a definição do Bynari Decision Diagram
(BDD) conhecida atualmente. Conceitualmente, um BDD é uma árvore de decisão que descreve
uma fórmula booleana, que obedece restrições de caminho da raiz à folha. Cada variável da
fórmula aparece uma única vez no BDD. Cada caminho representa uma atribuição às variáveis
da fórmula.
Um BDD é um grafo acíclico direcionado e possui dois tipos de vértices: não terminais
e terminais. Cada vértice representa uma variável V da fórmula booleana e possui duas arestas
de saída e uma de entrada, com exceção do vértice raiz, que possui apenas as arestas de saída,
e os vértices folhas, que possuem somente a aresta de entrada. A aresta de saída à esquerda de
um vértice representa que um valor falso foi atribuído à variável (V = 0), enquanto que a aresta
à direita representa a atribuição de um valor verdadeiro á variável (V = 1). Os vértices folhas do
32
grafo, indicam o valor para um determinado caminho (SEGALL; TZOREF-BRILL; FARCHI,
2011).
A fim de maximizar os compartilhamentos de nós, os BDDs passam por um processo
de redução, em que, a fórmula booleana é representada por um ponteiro para o seu nó raiz.
O processo de redução elimina todos os nós com filhos isomórficos e realiza a combinação de
todas as subárvores isomórficas. Como resultado será produzido um grafo acíclico direcionado.
Árvores de decisão possuem 2n caminhos distintos (onde n é o número de variáveis). Através do
processo de redução dos BDDs, há uma redução significativa na quantidade de caminhos para
representar uma fórmula booleana (BRYANT, 1986; SEGALL; TZOREF-BRILL; FARCHI,
2011).
O processo de simplificação faz com que o BDD possua apenas dois vértices terminais
rotulados 0 e 1. Esses valores que representam f also - a fórmula booleana não foi satisfeita -,
e verdadeiro - a fórmula booleana foi satisfeita. Para cada associação de valores às variáveis
booleanas da fórmula, existe um caminho no BDD partindo do vértice raiz para um dos vértices
terminais. A Figura 10 ilustra o BDD gerado para a fórmula (x⊗ y⊗ z) juntamente com sua
respectiva redução.
Figura 10: Construção de BDD
Fonte: Clarke, Grumberg e Peled (1999)
Um BDD é uma representação canônica para fórmulas booleanas, o que significa que
33
duas fórmulas serão logicamente equivalentes se tiverem BDDs isomórficos.
Como descrito por (BRYANT, 1986), uma desvantagem dos BDDs é que eles são sen-
síveis ao ordenamento de suas variáveis. Para uma fórmula booleana, o tamanho do BDD está
diretamente relacionado à ordenação das variáveis. O BDD pode crescer de linear para expo-
nencial dependendo do número de variáveis existentes na fórmula. O problema de ordenar as
variáveis de forma a minimizar o BDD é um problema NP-completo, e existem heurísticas para
otimizar a ordenação das variáveis, porém pode haver casos em que é necessário realizar essa
ordenação manualmente (BRYANT, 1986).
2.2.3 Lógica Temporal
A análise de estruturas Kripke exige um formalismo que permite descrever e analisar seu
comportamento a partir do comportamento das proposições atômicas ao longo das trajetórias.
Tal formalismo é uma lógica temporal (BLACKBURN, 1993).
Para a lógica temporal, o tempo é a descrição das sequências em que as proposições
atômicas vão sendo obedecidas à medida que as possíveis trajetórias evoluem. Por exemplo,
dada a estrutura da Figura 9, pode-se afirmar que o forno somente irá aquecer após a porta estar
fechada. Entretanto, nada pode ser dito com relação ao tempo necessário entre a porta fechar e
o forno aquecer (Y.; ROZIER, 2011).
O verificador NuSMV utilizado pela abordagem apresentada neste trabalho provê a ve-
rificação no modelo em dois tipos de lógica temporal: as Linear Temporal Logic (LTL) e a
Computation Tree Logic (CTL). Entretanto, a abordagem proposta utiliza somente a lógica
CTL para construir expressões em lógica temporal. Como a lógica temporal CTL utiliza alguns
dos operadores da lógica temporal LTL, a seguir será dada uma breve explicação desta lógica
temporal e seus operadores, e em seguida uma explicação mais detalhada sobre lógica temporal
CTL (LOMUSCIO; PECHEUR; RAIMONDI, 2007; Y.; ROZIER, 2011).
As lógicas temporais CTL e LTL são um subconjunto da lógica temporal CTL*. Essas
duas lógicas são complementares, ou seja, uma propriedade descrita por meio da lógica tem-
poral LTL não pode ser verificada usando CTL. Reciprocamente, uma propriedade verificada
com a lógica temporal CTL não pode ser verificada através da LTL (CLARKE; LERDA, 2007;
LUTZ; WOLTER; ZAKHARYASHEV, 2008).
A LTL é uma lógica temporal que permite verificar as possíveis trajetórias de uma es-
trutura Kripke, onde a fórmula LTL é verificada sobre caminhos lineares. A fórmula será ver-
dadeira em um estado caso seja verdadeira em todos os caminhos a partir daquele estado. Os
operadores desta lógica descrevem eventos sobre um único caminho, e são mostrados - como
descrito por Clarke e Lerda (2007) - a seguir:
34
a) Fp (Lê-se "No futuro p"): Uma determinada propriedade p é satisfeita em um dos instan-
tes de tempo futuros;
b) Gp (Lê-se "Globalmente p"): Uma determinada propriedade p é satisfeita em todos os
instantes de tempo futuros;
c) pUq (Lê-se "p até que q"): Uma determinada propriedade p é satisfeita até que ocorra
um estado em que, uma propriedade q é satisfeita;
d) Xp (Lê-se "próximo p"): Uma determinada propriedade p é satisfeita no próximo estado.
A semântica de uma fórmula LTL pode ser definida através de uma trajetória infinita
σ = s0s1... de uma estrutura Kripke. O estado s0 representa o primeiro estado da trajetória, e
não necessariamente um estado inicial da estrutura. Primeiramente, define-se a seguinte notação
M,σ |= p significando que a propriedade p é válida ao longo da trajetória s da estrutura Kripke
M.
Por outro lado, a CTL é uma lógica temporal que permite verificar as possíveis tra-
jetórias de uma estrutura Kripke, onde a fórmula CTL é verdadeira tanto quando é satisfeita
em caminhos que iniciam a partir de um estado, ou quando é satisfeita em alguns caminhos.
A lógica temporal CTL combina os operadores da lógica temporal LTL e da Branching-Time
logic para validar uma determinada propriedade em uma estrutura Kripke. Os operadores da
Branching-Time Logic quantificam caminhos possíveis a partir de um determinado estado. Con-
forme descrito por Clarke e Lerda (2007) esses operadores são:
a) E (Lê-se "Existe um caminho"): torna a propriedade p verdadeira sempre que existir
alguma trajetória a partir do primeiro estado de s tal que p seja verdadeiro;
b) A (Lê-se "todos os caminhos"): torna a propriedade p verdadeira sempre que todas as
possíveis trajetórias a partir do primeiro estado de s satisfaçam p.
Seja f e g fórmulas CTL, a relação de satisfação |= é definida indutivamente como:
M,s |= p ⇔ p ∈ L(s)
M,s |= ¬ f ⇔M,s 6|= f
M,s |= f ∨g ⇔M,s |= f ou M,s |= g
M,s |= f ∧g ⇔M,s |= f e M,s |= g
M,s |= AF f ⇔ para todos os caminhos partindo de s,sk ∈ S é alcançável e sk |= f
M,s |= EF f ⇔ existe um caminho partindo de s,sk ∈ S é alcançável e sk |= f
M,s |= AG f ⇔ para todos os caminhos π = s0s1s2 . . . ,si |= f , para todo i≥ 0, e s0 = s
35
M,s |= EG f ⇔ existe um caminho π = s0s1s2 . . . ,si |= f , para todo i≥ 0, e s0 = s
M,s |= AX f ⇔ para todo sx tal que p(s,sk) seja definido, sk |= f
M,s |= A[ fUg] ⇔ para todo caminho π = s0s1s2 . . .sk . . . ,si |= f , para todo 0≤ i< k e sk |= g
M,s |= E[ fUg] ⇔ existe um caminho π = s0s1s2 . . .sk . . . ,si |= f , para todo 0≤ i< k e sk |= g
A semântica de uma fórmula CTL, para uma estrutura Kripke M = (S,s0,R,λ ), em que
s0 ∈ S é um estado de M e σ = s0s0+1..., é uma trajetória infinita a partir do estado s0, tem as
seguintes representações:
a) M, s |= f significa que f é válida ao longo da trajetória s da estrutura Kripke M. Portanto,
f é denominada uma fórmula de caminho;
b) M, s0 |= f significa que f é válida no estado s0 da estrutura Kripke M. Portanto, f é
denominada uma fórmula de estado.
A Figura 11 apresenta sequências de estados que obedecem algumas fórmulas CTL
básicas (CLARKE; GRUMBERG; PELED, 1999).
Figura 11: Estados que obedecem a fórmulas CTL básicas
Fonte: Clarke, Grumberg e Peled (1999)
36
2.2.4 A Linguagem NuSMV
O NuSMV é uma ferramenta de verificação de especificações descritas em lógica tem-
poral CTL* sobre sistemas de estados finitos. Essa seção apresenta os princípios da linguagem
usada por esse verificador utilizados neste trabalho. O NuSMV foi desenvolvido a partir da
reengenharia do Symbolic Model Verifier (SMV) (CAVADA et al., 2011), a descrição completa
de suas funcionalidades pode ser encontrada em (CIMATTI et al., 1999).
A linguagem do NuSMV permite descrever sistemas computacionais síncronos e assín-
cronos através de um sistema de transição de estados. Ela também provê a descrição de módulos
hierárquicos e a definição de componentes reutilizáveis. A linguagem trabalha com dados do
tipo escalar finito, porém também permite a criação de estruturas de dados estáticos.
O NuSMV utiliza os algoritmos de verificação baseados em Ordered Binary Decision
Diagrams (OBDD) a fim de determinar com precisão quando uma especificação expressa em
linguagem CTL é ou não satisfeita. Como mostrado na seção anterior, a CTL possibilita des-
crever as propriedades temporais de forma rica, precisa e concisa (LOMUSCIO; PECHEUR;
RAIMONDI, 2007).
A linguagem de entrada do verificador NuSMV tem como objetivo proporcionar uma
descrição simbólica formal das transição de estados em uma estrutura Kripke. A linguagem
possui grande flexibilidade, pois permite que qualquer fórmula de proposições possa ser utili-
zada para descrever as relações de transição da estrutura Kripke. Porém, isso também representa
um certo risco de inconsistências. Por exemplo, a presença de contradições lógicas pode resultar
em um ou mais estados sem nenhum sucessor.
Um programa NuSMV pode ser comparado a um conjunto de equações executadas si-
multaneamente, em que, a solução dessas equações irá determinar o próximo estado. O compi-
lador do verificador irá assegurar que em cada estado ocorra apenas uma atribuição para cada
variável e que o programa não possui dependências circulares ou erros de tipagem.
A seguir são apresentados alguns exemplos, retirados de (NUSMV, 2011), para ilustrar
os conceitos básicos da linguagem.
2.2.5 Módulo Main
Considere o exemplo no Quadro 2. Esse exemplo mostra um modelo - linhas 1 a 10 -,
e uma especificação CTL - Linha 11. No modelo, os estados da estrutura Kripke são definidos
por uma coleção de variáveis, que podem ser booleanas, do tipo escalar, ou números inteiros.
A declaração dessas variáveis é realizada através da instrução VAR. O exemplo mostra a de-
claração das variáveis: request, do tipo boolean, e state, do tipo escalar, que podem receber os
valores ready ou busy, respectivamente.
37
Quadro 2: Exemplo de um arquivo de entrada NuSMV
1 MODULE main
2 VAR
3 r e q u e s t : boo l e an ;
4 s t a t e : { ready , busy } ;
5 ASSIGN
6 i n i t ( s t a t e ) := r e ady ;
7 nex t ( s t a t e ) := case
8 s t a t e = r eady & r e q u e s t : busy ;
9 1 : { ready , busy } ;
10 e s a c ;
11 SPEC AG( r e q u e s t −> AF s t a t e = busy )
Embora a linguagem permita que o usuário utilize variáveis escalares para definir abs-
trações no modelo onde uma variável em um estado possa possuir valores além de 0 e 1, o
compilador transforma os valores das variáveis escalares em coleções de variáveis booleanas,
de modo que cada transição de estados continue sendo representada através de um BDD.
A instrução ASSIGN determina as relações de transição da estrutura Kripke e os estados
iniciais. Essas transições de estado são definidas por meio de um conjunto de atribuições que
ocorrem em paralelo.
A inicialização de uma variável é realizada através da instrução init. No exemplo, a
variável state é inicializada com o valor ready. Se houver uma variável no modelo não iniciali-
zada por meio da instrução init, o compilador irá inicializá-la com um valor, dentre seu domínio
de dados, que é escolhido aleatoriamente.
O valor de uma variável no próximo estado é determinado através da instrução next.
No exemplo, o valor da variável state no próximo estado depende do resultado da expressão
booleana contida na instrução case do Quadro 3:
Quadro 3: Exemplo de uma instrução case
1 case
2 s t a t e = r eady & r e q u e s t : busy ;
3 1 : { ready , busy } ;
4 e s a c ;
O resultado da instrução case é determinado pela expressão do lado direito dos dois
pontos (:), desde que a expressão booleana do lado esquerdo seja satisfeita. Portanto, se o valor
da variável state for igual à ready e o da variável request for igual à true, então o resultado
da expressão booleana será busy, caso contrário o resultado é um dos valores {ready,busy}
38
escolhido de forma não determinística, ou seja, aleatoriamente.
Escolhas não determinísticas são úteis para descrever sistemas que ainda não estão com-
pletamente implementados, ou para abstrair modelos complexos em que o valor de algumas
variáveis não pode ser precisamente determinado.
Note no exemplo que a variável request não recebe nenhuma atribuição de valores, seja
por meio da instrução case seja por meio da instrução init. Dessa forma, em qualquer transição
de estados, o verificador irá atribuir a variável request um valor escolhido aleatoriamente. Caso
contrário, o recurso esta sendo utilizado por outro processo.
O programa exemplo descrito no Quadro 2 representa processos que utilizam um recurso
concorrentemente. Quando a variável request tiver o valor 1 e a variável state possuir o valor
ready significa que o processo esta pronto para utilizar o recurso, então a instrução next irá
atribuir o valor busy a variável state, indicando que no próximo estado o recurso estrá sendo
utilizado por aquele processo.
A instrução SPEC define a propriedade a ser verificada no modelo:
SPEC AG(request -> AF state = busy)
O verificador irá percorrer todos os estados alcançáveis analisando se a propriedade é
satisfeita ou não. No exemplo, a propriedade, sendo validada, é: para todos os estados do
modelo, sempre que a variável request for verdadeira, haverá algum estado posterior em que a
variável state será igual a busy?
2.2.6 Módulos Reutilizáveis
Um módulo reutilizável no NuSMV é definido da mesma forma que o módulo de nome
main. Porém, o módulo main tem um significado especial para o compilador, uma vez que é
esse o módulo executável do arquivo de entrada. A ordem em que os módulos são definidos no
programa não interfere na sua execução. O exemplo no Quadro 4 ilustra um modelo para um
contador binário de 3 bits.
Um módulo definido pelo usuário pode ser reutilizado através da criação de instâncias
daquele módulo. Uma instância é criada a partir da declaração de uma variável com o tipo
equivalente ao nome do módulo. No exemplo, o módulo counterCell é instanciado três vezes
para as variáveis bit0, bit1 e bit2.
Note que o parâmetro de entrada carryIn do módulo counterCell é iniciado com 1 na
declaração da variável bit0, enquanto que a variável bit1 recebe como valor do parâmetro a
expressão definida por carryOut da variável bit0, e da mesma forma a variável bit2 recebe
como valor do parâmetro a expressão definida por carryOut da variável bit1.
39
A instrução DEFINE permite que a atribuição à expressão value&carryIn para o sím-
bolo carryOut seja possível. O efeito dessa instrução é equivalente ao Quadro 5:
Quadro 4: Exemplo de programa NuSMV com módulos reutilizáveis
1 MODULE main
2 VAR
3 b i t 0 : c o u n t e r C e l l ( 1 ) ;
4 b i t 1 : c o u n t e r C e l l ( b i t 0 . c a r r yOu t ) ;
5 b i t 2 : c o u n t e r C e l l ( b i t 1 . c a r r yOu t ) ;
6 SPEC
7 AG AF b i t 2 . c a r r yOou t
8 MODULE c o u n t e r C e l l ( c a r r y I n )
9 VAR
10 va l u e : boo l e an ;
11 ASSIGN
12 i n i t ( v a l u e ) := 0 ;
13 nex t ( v a l u e ) := v a l u e + c a r r y I n mod 2 ;
14 DEFINE
15 c a r r yOu t := v a l u e & c a r r y I n ;
Quadro 5: Exemplo de programa NuSMV
1 VAR
2 c a r r yOu t : boo l e an ;
3 ASSIGN
4 c a r r yOu t := v a l u e & c a r r y I n ;
A instrução DEFINE faz com que a expressão carryOut receba o valor corrente das variáveis,
ao invés do próximo valor das variáveis. Porém, a instrução DEFINE não realiza a atribuição de valores
não determinísticos.
2.2.7 Contraexemplo
Se alguma propriedade do modelo não for atendida, o verificador apresentará um contraexemplo
que prove que a propriedade é falsa. Isso nem sempre é possível, já que fórmulas precedidas pelo quan-
tificador de caminho E não podem ser provadas como falsas, apenas apresentando um único caminho
em que a especificação é falsa. Por analogia, fórmulas precedidas pelo quantificador de caminho A não
podem ser provadas como verdadeiras, apenas apresentando um único caminho em que a especificação é
verdadeira. Além disso, algumas fórmulas requerem infinitos caminhos de execução como contraexem-
40
plos. Nesse caso, o verificador de modelos apresenta um caminho cíclico (em loop), incluindo o estado
inicial do ciclo (HAN; KATOEN; BERTEUN, 2009).
No contraexemplo, são exibidas as combinações de valores das variáveis que compõem um es-
tado de verificação. Não existem estados repetidos, portanto cada estado possui uma combinação única
de valores de variáveis, como pode ser visto no exemplo abaixo:
-> State: 1.1 <-
a = TRUE;
b = TRUE;
-> State: 1.2 <-
a = FALSE;
b = FALSE;
Esse contraexemplo foi gerado a partir da verificação da propriedade EX a!= b sobre o modelo
mostrado no Quadro 6.
Quadro 6: Exemplo de programa NuSMV
1 MODULE main
2 VAR a : boo l e an ;
3 b : boo l e an ;
4 INVAR( a=b ) ;
5 ASSIGN
6 nex t ( b ) := ! b ;
41
3 TRABALHOS RELACIONADOS
Com intuito de garantir qualidade dos diagramas modelados através da UML diversas aborda-
gens de aplicação de técnicas formais têm sido propostas pela literatura. Bhaduri e Ramesh (2004)
realizaram um levantamento de diversas abordagens existentes de aplicação de técnicas formais para
verificação de diagramas da UML.
Através do trabalho (BHADURI; RAMESH, 2004), o autores concluem que a maioria das abor-
dagens depende da tradução do modelo para a linguagem de entrada do verificador formal utilizado. Isso
dificulta a utilização dos trabalhos desenvolvidos na indústria de software, devido à dificuldade de rea-
lizar a transformação dos modelos em um padrão formal. Nesta dissertação esse problema foi resolvido
com a automação do processo de tradução dos diagramas.
A maior parte dos trabalhos que utilizam técnicas formais para validar modelos da UML foram
realizados nos diagramas de estado. No trabalho de Lilius e Paltor (1999), é apresentado à ferramenta
vUML, que verifica automaticamente o comportamento dos objetos do diagrama de estados. A ferra-
menta proposta utiliza o verificador formal SPIN. vUML pode encontrar seis diferentes tipos de erros,
incluindo deadlocks e livelocks, quando um erro é encontrado a ferramenta gera um diagrama de sequên-
cia da UML mostrando como reproduzir o erro no modelo. O processo de execução da ferramenta
vUML é o seguinte: depois de criar o modelo, o engenheiro chama vUML para verificá-lo. A ferramenta
converte automaticamente o modelo UML em uma especificação PROMELA e invoca SPIN. Então, a
verificação é realizada por SPIN sem interação do engenheiro. Se a verificação falhar, é gerado um con-
traexemplo que mostra como reproduzir o erro no modelo. Dessa forma, o engenheiro pode estudar estes
diagramas e corrigir o erro no modelo. Este processo pode ser repetido até que o modelo esteja correto.
Os autores Dubrovin e Junttila (2008) definem uma semântica e codificação formal para o di-
agrama de estados, com intuito de verificar a lógica de comunicação entre os elementos do diagrama.
Os resultados obtidos através de experimentos demonstram os benefícios de realizar verificações em
modelos, antes que os mesmos sejam codificados.
Choppy, Klai e Zidani (2011) citam a importância de fornecer técnicas de verificação formal
de diagramas UML e propõem traduzir diagrama de estados para Petri nets onde algumas propriedades
podem ser verificadas automaticamente. O trabalho abstrai o processo de verificação, permitindo que o
engenheiro especifique o sistema através de diagramas de estado e então automaticamente a ferramenta
realize a tradução dos modelos para redes de Petri, permitindo a aplicação da técnica para análise poste-
rior. Uma vez que esta análise é realizada, o resultado pode ser devolvido para o engenheiro. Em caso de
42
insucesso, um contraexemplo é gerado e retornado para o engenheiro corrigir o modelo UML e reiniciar
a verificação. Para ilustrar a abordagem proposta foi realizado um estudo de caso, onde as propriedades
verificadas foram expressas através da LTL.
Também existem trabalhos voltados para os diagramas de atividades. No trabalho de Eshuis
(2006), o autor aplica a verificação formal no diagrama de atividade da versão 1.5 da UML. Neste tra-
balho são propostos dois tipos de tradução do diagrama de atividades para linguagem de entrada do
verificador formal NuSMV. As traduções são utilizadas para verificar as transições entre as atividades.
Outra contribuição deste trabalho é a definição de restrições de integridade dos dados para um conjunto
de diagramas de classes que descrevem os dados manipulados nas atividades.
Já no trabalho de Xu, Miao e Philbert (2009) é apresentado uma ferramenta que formaliza o
diagrama de atividades para a técnica formal CSP. Neste trabalho é considerado um subconjunto de
elementos do diagrama de atividades como, por exemplo, ações, paralelismo, ramificações e atividades.
Os diagramas de atividades da UML foram analisados, em seguida, algumas definições formais foram
aplicadas nos modelos. Logo após, foram realizados os mapeamentos do diagrama de atividade para
CSP. A aplicação do trabalho é realizada utilizando um estudo de caso do tipo ilustrativo.
Os autores Knapp e Wuttke (2006) descrevem uma proposta de tradução das interações da UML
2.0 em autômatos, para verificar se um determinado conjunto de troca de mensagem do diagrama de
estado da UML está correto. A tradução suporta interações básicas, invariantes de estado e ramificações.
A tradução é integrada a ferramenta de verificação formal HUGO/RT.
Enquanto os autores Mokhati, Gagnon e Badri (2007), apresentam uma abordagem formal de
apoio à tradução automática de diagramas UML em uma especificação formal, baseada na linguagem
Maude e a verificação de propriedades através de LTL, usando verificador de modelos Maude integrado.
O trabalho considera características estáticas e dinâmicas de sistemas orientados a objetos. A abordagem
é organizada em quatro etapas principais. A primeira etapa consiste em descrever as características está-
ticas e dinâmicas de um sistema orientado a objetos usando os diagramas de classe, estado e diagramas
de comunicação. A segunda etapa corresponde a um processo de validação dos diagramas. Uma vez
que todos os elementos do modelo utilizado na nossa abordagem podem ser capturados em Maude, no
terceiro passo, é gerada automaticamente uma descrição Maude do considerado modelo UML. O quarto
passo consiste em verificar algumas propriedades usando LTL e verificador de modelo Maude.
Já no trabalho (SOEKEN et al., 2010) é proposto uma abordagem semiautomática para verificar
modelos UML/OCL aplicando técnicas de satisfabilidade. Os autores também realizam comparação de
desempenho com trabalhos desenvolvidos anteriormente, através desta comparação foi possível verifi-
car que o trabalho proposto resolve de forma mais rápida as verificações propostas. Além da técnica
utilizada, pode-se destacar que a dissertação desenvolvida realiza a verificação de forma automática,
43
enquanto o trabalho de Soeken et al. (2010) é de forma semiautomática.
Beato et al. (2005) apresentam uma ferramenta que evita o custo de aprendizagem de técnicas
formais, permitindo realizar de forma automática verificações em modelos UML por meio de técnicas de
método formal. A ferramenta incorpora um assistente para a verificação, que atua como um guia para o
usuário, onde é possível escrever propriedades de validações através de lógica temporal. A ferramenta re-
aliza, sem nenhuma intervenção por parte do usuário, transformação automática do modelo especificado
em UML para uma especificação SMV, focando principalmente em sistemas reativos em que o modelo
de comportamento das classes são representados através de diagramas de estado, enquanto o diagrama
de atividade é utilizado para refletir o comportamento das operações da classe. XMI é usado como o
formato de entrada, tornando-o independente da ferramenta utilizada para a especificação do modelo.
Finalmente, no trabalho de Barros e Song (2011), é abordado o tema de verificação de mode-
lagens de negócio com intuito de antecipar inconsistências que podem representar custos no desenvol-
vimento e ao longo da vida útil do software. Os autores apresentam uma abordagem e uma ferramenta
para a realização de verificações de regras de execução de atividades, seu sequenciamento e interdepen-
dências, podendo ser automatizado por meio de uma interface que abstrai grande parte da complexidade
do processo, aumentando assim a aplicabilidade da técnica. A ferramenta tem como público-alvo os
profissionais especialistas em análise de negócio, foi importante que essa não exigisse conhecimentos
específicos de verificação de modelos, linguagens de programação ou lógica temporal. Pode-se desta-
car neste trabalho a identificação dos casos de tradução, representando as possibilidades de variação de
comportamento da execução de fluxos de trabalho e as validações possíveis. A maior limitação do traba-
lho é quanto à aplicabilidade da ferramenta se refere à possibilidade de execução infinita dos ciclos não
encapsulados.
Ressalta-se, no entanto, que o presente trabalho apresenta um arcabouço para realizar a verifica-
ção automática dos diagramas de estado, atividades e sequência que fazem parte do grupo dos diagramas
comportamentais da UML. Além disso, o trabalho apresenta uma ferramenta que encapsula toda uma
metodologia, tendo definido como público-alvo os engenheiros de software que não possuam conheci-
mento em Lógica Temporal e Verificação Formal.
Através do levantamento de trabalhos relacionados foi possível identificar algumas limitações
e trabalhos a serem desenvolvidos. As pesquisas citadas não ressaltam como é realizado a tradução da
UML para o SMV, além de possuírem limitação quanto à quantidade de modelos da UML que são capa-
zes de realizar verificação. Geralmente os trabalhos são focados nos diagramas de estados e atividades
da UML devido a grande proximidade deste diagrama com o BDD. O trabalho proposto pretende ofe-
recer como diferencial uma maior abrangência de modelos da UML, além de oferecer transparência em
realizar verificação nos modelos utilizando SMV.
44
4 METODOLOGIA FORMAL PARA VERIFICAÇÃO DE DIAGRAMAS DA UML
Este capítulo apresenta a metodologia formal desenvolvida para realizar validações nos diagra-
mas de atividade, estado e sequência da UML através de um arcabouço que utiliza a Verificação Simbó-
lica de Modelos. A Figura 12 ilustra todo o processo de execução que envolve a metodologia.
Figura 12: Metodologia formal
Fonte: Elaborada pelo autor
A metodologia é divida em três etapas: especificação, verificação e resultados. A etapa de espe-
cificação é composta pelo engenheiro de software, ferramentas UML, arquivo no formato XMI e pelas
propriedades de validações. O primeiro passo nessa etapa é a realização da modelagem dos diagramas
pelo engenheiro de software nas ferramentas UML disponíveis no mercado (e.g., Rational, Astah, etc.).
Em seguida gera-se a descrição dos diagramas em formato XMI. Além disso, nessa etapa o engenheiro de
software seleciona, nas propriedades de validações, as regras que deseja verificar no diagrama modelado.
As verificações que compõem as propriedades de validações são detalhadas na seção 4.2.
A etapa seguinte é a de verificação composta de: tradução XMI para SMV, arquivo SMV, con-
versão das propriedades para lógica temporal, arquivo de lógica temporal e verificação automática. Essa
etapa inicia logo que o arcabouço recebe, da etapa de especificação, o arquivo XMI e as propriedades
de validações. De posse destas informações, realiza-se a tradução do arquivo XMI, que representa o
diagrama modelado, para a Verificação Simbólica de Modelos, gerando assim o arquivo SMV. Os de-
talhes das traduções estão descritos na seção 4.1. Em seguida, ocorre a conversão das propriedades de
45
validação para lógica temporal. Logo após, faz-se a junção do arquivo SMV e da lógica temporal para
que seja realizada a verificação.
Na última etapa são apresentados os resultados, após o verificador formal realizar a validação.
Caso o diagrama satisfaça as propriedades especificadas pelo engenheiro de software o resultado obtido é
verdadeiro, em caso de sucesso, caso contrario contraexemplos são gerados. Neste caso o contraexemplo
descreve o motivo do diagrama não satisfazer as propriedades verificadas. A seguir são apresentadas as
traduções dos diagramas de estado, atividade e sequência.
4.1 Traduções
4.1.1 Tradução do Diagrama de Estado
Na tradução do diagrama de estados, os estados são agrupados em uma enumeração, cada even-
to/ação é traduzido para uma variável booleana e cada transição é representada pela instrução CASE
(Quadro 7).
Quadro 7 - Formalização do diagrama de estados
UML VSM Valor Inicial
Estado Enumeração Estado Inicial
Evento Variável Booleana Falso
Ação Variável Booleana Falso
Transição CASE -
Fonte: Elaborado pelo autor
A Figura 13 ilustra um diagrama de estado e o Quadro 8 representa a sua tradução para a Veri-
ficação Simbólica de Modelos. O diagrama é composto por dois estados: Idle e Running. Esses estados
são agrupados em uma enumeração denominada states, como descrito no Quadro 8, linha 3. Vale ressal-
tar que o estado inicial (i.e., representado por um círculo preto) não precisa ser enumerado, porque, uma
vez que não depende de qualquer outra execução, sempre irá ativar o estado subsequente. No entanto, é
necessário enumerar o estado final, porque o mesmo determina o término do fluxo. No exemplo tem-se
três eventos: keyPress, finished e shutDown. Cada evento é inicia com valor falso como mostrado na
linha 8-11.
O diagrama é incia ativando o evento Idle, como mostrado na linha 8, e os outros eventos podem
ser ativados por transições entre os estados. As transições são representadas por uma instrução CASE
(linhas 11-13).
46
Figura 13: Diagrama de estado
Fonte: Booch, Rumbaugh e Jacobson (2005)
Quadro 8: Diagrama de Estados
1 MODULE main
2 VAR
3 s t a t e s : { i d l e , runn ing , f i n a l } ;
4 keyP r e s s : boo l e an ;
5 f i n i s h e d : boo l e an ;
6 shutdown : boo l e an ;
7 ASSIGN
8 i n i t ( s t a t e s ) := i d l e ;
9 i n i t ( k eyP r e s s ) := f a l s e ;
10 i n i t ( f i n i s h e d ) := f a l s e ;
11 i n i t ( shutdown ) := f a l s e ;
12 nex t ( s t a t e s ) := case
13 keyP r e s s : r unn i ng ;
14 f i n i s h e d : i d l e ;
15 shutdown : f i n a l ;
16 1 : s t a t e s ;
17 e s a c ;
4.1.2 Tradução do Diagrama de Atividade
A Figura 14 ilustra um diagrama de atividades simples que será traduzido para a Verificação
Simbólica de Modelos. Na tradução do diagrama de atividades, cada atividade, estado inicial e estado
final são traduzidos em variáveis booleanas que representam se determinada atividade foi executada ou
não, como descrita no Quadro 9.
Quadro 9: Diagrama de Atividades - Declaração de variáveis
1 s e l e c i o n a r L o c a l : boo l e an ;
2 c o n t r a t a r A r q u i t e t o : boo l e an ;
3 e s t a d o F i n a l : boo l e an ;
47
Figura 14: Diagrama de atividade
Fonte: Booch, Rumbaugh e Jacobson (2005)
Logo após a declaração das variáveis, as mesmas precisam ser inicializadas, conforme o Quadro
10. Todas as variáveis são iniciadas com o valor falso, exceto a primeira atividade, neste caso Selecionar
local. Isto ocorre pelo fato desta atividade não depender de nenhuma outra atividade para ser executada.
Portanto, ela será imediatamente executada tão logo o diagrama seja iniciado.
Quadro 10: Diagrama de Atividades - Inicialização de variáveis
1 i n i t ( S e l e c i o n a r L o c a l ) := 1
2 i n i t ( C o n t r a t a r A r q u i t e t o ) := 0
3 i n i t ( F i n a l ) := 0
Após as declarações das variáveis e suas inicializações, as transições devem ser traduzidas. As
transições no diagrama de atividades podem ter diferentes comportamentos. Estas podem ser simples ou
representar uma decisão ou paralelismo. As traduções para estas transições serão apresentadas a seguir.
Transição Simples
Transições simples ocorrem quando uma atividade está completa e o fluxo de controle passa
imediatamente à próxima ação ou nó (Figura 14). Neste caso, a única condição para execução do estado
avaliado é a execução das atividades anteriores.
Por exemplo, no caso da atividade Contratar arquiteto, se esta já foi executada anteriormente,
será mantido o valor verdadeiro (Quadro 11 - linha 2). Por outro lado, se a atividade Contratar arquiteto
ainda não foi executada, mas a atividade Selecionar local o foi, então Contratar arquiteto então assumirá,
nesta transição, o valor verdadeiro (linha 3). Em todos os outros casos será mantido o valor falso para o
estado (linha 4).
Quadro 11: Transição Simples
1 nex t ( c o n t r a t a r A r q u i t e t o ) := case
2 c o n t r a t a r A r q u i t e t o = 1 : 1 ;
3 c o n t r a t a r A r q u i t e t o = 0 & s e l e c i o n a r L o c a l = 1 : 1 ;
48
4 1 : 0 ;
5 e s a c ;
Objetos de Decisão
O diagrama de atividade pode conter objetos condicionais baseados em expressões booleanas,
como demonstra a Figura 15. Portanto, o verificador deve avaliar a validade das afirmativas lógicas
temporais, considerando todos os caminhos possíveis.
Figura 15: Objeto de decisão
Fonte: Booch, Rumbaugh e Jacobson (2005)
Dessa forma, para avaliar as atividades que estão envolvidas em condicionais é necessário imple-
mentar no modelo a ser verificado as características de não determinismo quanto à escolha dos caminhos
que serão percorridos. Para exemplificar o não determinismo no diagrama representado pela Figura 15
apresenta-se a tradução conforme o Quadro 12 - linha 4. Pode-se notar a adoção de regras para garantir
a permanência de valores atribuídos anteriormente e o não determinismo indicando os demais casos.
Quadro 12: Objeto de Decisão
1 nex t ( a t r i b u i r ) := case
2 a t r i b u i r = 1 : 1 ;
3 l i b e r a r = 1 & rep r og r ama r = 1 : 0 ;
4 l i b e r a r = 1 : {0 , 1} ;
5 1 : 0 ;
6 e s a c ;
7 nex t ( r e p r og r ama r ) := case
8 r e p r og r ama r = 1 : 1 ;
9 l i b e r a r = 1 & ( a t r i b u i r = 1 | n ex t ( a t r i b u i r = 1 ) ) : 0 ;
10 l i b e r a r = 1 & a t r i b u i r = 0 : 1 ;
11 1 : 0 ;
12 e s a c ;
Outro caso que pode ocorrer na utilização de condicionais são os múltiplos objetos de decisão
interligados, conforme representado na Figura 16. Neste caso a solução é mais complexa se comparado
49
com aquele em que o objeto de decisão está isolado entre as atividades. Dessa forma, é necessário
determinar as inferências entre cada elemento envolvido. O Quadro 13 linhas 8 e 14-15 descrevem a
tradução.
Figura 16: Múltiplos objetos de decisão conectados
Fonte: Elaborada pelo autor
Quadro 13: Múltiplos Objetos de Decisão Conectados
1 nex t ( a t i v i d a d eB ) := case
2 a t i v i d a d eB = 1 : 1 ;
3 a t i v i d a d eA = 1 & a t i v i d a d eB = 0 & ( a t i v i d a d eC = 0 & a t i v i d a d eD = 0) : {0 ,
1} ;
4 1 : 0 ;
5 e s a c ;
6 nex t ( a t i v i d a d eC ) := case
7 a t i v i d a d eC = 1 : 1 ;
8 a t i v i d a d eA = 1 & ( a t i v i d a d eB = 1 | n ex t ( a t i v i d a d eB = 1) ) : 0 ;
9 a t i v i d a d eA = 1 & a t i v i d a d eC = 0 & a t i v i d a d eD = 0 : {0 , 1} ;
10 1 : 0 ;
11 e s a c ;
12 nex t ( a t i v i d a d eD ) := case
13 a t i v i d a d eD = 1 : 1 ;
14 a t i v i d a d eA = 1 & ( a t i v i d a d eB = 1 | n ex t ( a t i v i d a d eB = 1) | a t i v i d a d eC = 1 |
n ex t ( a t i v i d a d eC = 1) ) : 0 ;
15 a t i v i d a d eA = 1 & a t i v i d a d eB = 0 & a t i v i d a d eC = 0 & a t i v i d a d eD = 0 : 1 ;
16 1 : 0 ;
17 e s a c ;
18 nex t ( a t i v i d a d eE ) := case
50
19 a t i v i d a d eE = 1 : 1 ;
20 a t i v i d a d eB = 1 | a t i v i d a d eC = 1 | a t i v i d a d eD = 1 : 1 ;
21 1 : 0 ;
22 e s a c ;
Outro comportamento do componente de ramificação ocorre quando um dos caminhos se liga a
alguma das outras atividades imediatamente posteriores à divisão do fluxo, conforme Figura 17 na cone-
xão entre as atividades Atividade W para Atividade Y. Tal ocorrência necessita de avaliação específica,
pois afeta de maneira singular as condições de execução da atividade que foi ligada pelo desvio. Esta
situação é traduzida como mostra o Quadro 14.
Figura 17: Conexão entre caminhos
Fonte: Elaborada pelo autor
Quadro 14: Conexão entre caminhos
1 nex t ( a t i v i d a d eY ) := case
2 a t i v i d a d eY = 1 : 1 ;
3 a t i v i dadeW = 1 : 1 ;
4 a t i vX = 1 & a t i v i d a d eY = 0 & a t i v i d a d eZ = 0 : {0 , 1} ;
5 1 : 0 ;
6 e s a c ;
7 nex t ( a t i v i d a d eZ ) := case
8 a t i v i d a d eZ = 1 : 1 ;
9 a t i vX = 1 & ( a t i v i d a d eY = 1 | n ex t ( a t i v i d a d eY = 1) ) : 0 ;
10 a t i vX = 1 & a t i v i d a d eY = 0 : 1 ;
11 1 : 0 ;
12 e s a c ;
13 nex t ( a t i v i dadeW ) := case
14 a t i v i dadeW = 1 : 1 ;
15 a t i v i d a d eZ = 1 : 1 ;
51
16 1 : 0 ;
17 e s a c ;
Paralelismo
O diagrama de atividades também pode conter fluxos de execução paralelos como demonstrada
pela Figura 18. Neste caso trata-se tanto das atividades iniciais do paralelismo quanto das atividades em
que o paralelismo se encerra. Tais ocorrências são as únicas dependentes de um tratamento específico,
sendo que os elementos intermediários dos caminhos paralelos são tratados de maneira genérica. O
Quadro 15 realiza a tradução para este caso.
Figura 18: Transições paralelas
Fonte: Booch, Rumbaugh e Jacobson (2005)
Quadro 15: Transições Paralelas
1 nex t ( s i ncBoca ) := case
2 de scompac t a r = 1 : 1 ;
3 1 : 0 ;
4 e s a c ;
5 nex t ( em i t i rAud i o ) := case
6 de scompac t a r = 1 : 1 ;
7 1 : 0 ;
8 e s a c ;
4.1.3 Tradução do Diagrama de Sequência
A Figura 19 ilustra um diagrama de sequência que será traduzido para a Verificação Simbólica
de Modelos. Na conversão, cada mensagem é traduzida para uma variável booleana que representa se
52
determinada a mesma foi executada ou não (Quadro 16).
Figura 19: Diagrama de sequência
Fonte: Booch, Rumbaugh e Jacobson (2005)
Quadro 16: Diagrama de Sequência Simples - Declaração de variáveis
1 a c t o r−submi tOrde r : boo l e an ;
2 o rde rTake r−p r o c e s sCa r d : boo l e an ;
3 o rde rTake r−p l a c eO rd e r : boo l e an ;
4 o r d e r F u f i l lm e n t− t r i g g e r B i l : boo l e an ;
5 o r d e r F u f i l lm e n t−acknowledgeOrder : boo l e an ;
Logo após a declaração das variáveis, as mesmas necessitam ser inicializadas, conforme Qua-
dro 17. Todas as variáveis são inicializadas com valor falso, exceto a primeira mensagem, neste caso
Submit Order. Isto ocorre pelo fato desta mensagem não depender de nenhuma outra atividade para ser
executada. A primeira mensagem será imediatamente executada logo que o diagrama seja inicializado.
Quadro 17: Inicialização das variáveis
1 i n i t ( a c t o r−submi tOrde r ) := 1 ;
2 i n i t ( o rde rTake r−p r o c e s sCa r d ) := 0 ;
3 i n i t ( o rde rTake r−p l a c eO rd e r ) := 0 ;
4 i n i t ( o r d e r F u f i l lm e n t− t r i g g e r B i l ) := 0 ;
5 i n i t ( o r d e r F u f i l lm e n t−acknowledgeOrder ) := 0 ;
Após a declaração e inicialização das variáveis, é gerada a tradução para as transições entre as
mensagens. Neste trabalho foi gerada a tradução para a transição simples, transição paralela e transição
condicional.
53
Transição Simples
Transição simples é a transição comum. Ocorre quando uma mensagem já foi executada e o
fluxo passa para a próxima mensagem da sequência, conforme a Figura 19. Portanto, a única condição
para a execução da próxima mensagem é a execução das mensagens anteriores.
Por exemplo, no caso da mensagem Process card, se esta mensagem já foi executada anterior-
mente, será mantido o valor verdadeiro (Quadro 18 - linha 2). Por outro lado, se a mensagem Process
card ainda não foi executada, mas a mensagem Submit Order já foi executada, então a mensagem Pro-
cess card irá assumir nesta transição o valor verdadeiro (Quadro 18 - linha 3). Em todos os outros casos
o valor falso será mantido para a mensagem (Quadro 18 - linha 4).
Quadro 18: Transição simples
1 nex t ( o rde rTake r−p r o c e s sCa r d ) := case
2 o rde rTake r−p r o c e s sCa r d = 1 : 1 ;
3 o rde rTake r−p r o c e s sCa r d = 0 & ac t o r−submi tOrde r = 1 : 1 ;
4 1 : 0 ;
5 e s a c ;
Transição Condicional
O diagrama de sequência pode conter um grupo de mensagens que depende de uma determinada
condição para serem executadas, como ilustra a Figura 20. Quando o diagrama contém a sigla OPT
significa que este diagrama contém uma condicional. Para este trabalho a condição é tratada como uma
variável booleana que representa se a condição esta satisfeita assumindo valor verdadeiro e falso se a
condição não esta satisfeita.
Portanto, quando avaliam-se mensagens que estão envolvidas em condicionais é necessário im-
plementar no modelo a ser verificado se a condicional esta satisfeita ou não. Para exemplificar a condição
demonstrada pelo diagrama, representado na Figura 20, foi gerada a tradução conforme o Quadro 19.
Pode-se notar que para a mensagem Deliver Cash receber o valor verdadeiro é realizado uma verificação
se a condição Valid Password esta satisfeita (Quadro 19 - linha 3).
Quadro 19: Condicional
1 nex t ( d e l i v e rC a s h ) := case
2 d e l i v e rC a s h = 1 : 1 ;
3 d e l i v e rC a s h = 0 & en t e rAccoun t = 1 & enterAmount = 1 & va l i dP a s swo r d =
1 : TRUE;
4 1 : 0 ;
5 e s a c ;
54
Figura 20: Parelismo e condicional
Fonte: Booch, Rumbaugh e Jacobson (2005)
Paralelismo
O diagrama de sequência pode conter execução de mensagens em paralelo, como demonstrado
pela Figura 20. Neste caso trata-se tanto das mensagens iniciais do paralelismo quanto das mensagens
em que o paralelismo se encerra. Tais ocorrências são únicas dependentes de um tratamento específico,
sendo que as mensagens intermediárias dos caminhos paralelos são tratadas de maneira genérica. O
Quadro 20 realiza a tradução para este caso.
Quadro 20: Paralelismo
1 nex t ( e n t e rAccoun t ) := case
2 l a s tMe s s a g e = 1 : 1 ;
3 1 : 0 ;
4 e s a c ;
5 nex t ( en terAmount ) := case
6 l a s tMe s s a g e = 1 : 1 ;
7 1 : 0 ;
8 e s a c ;
4.2 Verificações
4.2.1 A execução de uma atividade/mensagem/estado implica na execução de outra
A Figura 21 representa a transição de estados necessária para a verificação deste tipo de valida-
ção. Considerando que a variável X representa a primeira atividade escolhida e Y a segunda, o status 1
55
representa a execução da atividade enquanto 0 representa que esta não foi executada. Dessa forma, no
estado inicial, indicado por um arco superior, ambas as atividades não foram executadas. Na sequência, a
atividade X deve ser executada enquanto a Y permanece não executada. Posteriormente, em algum mo-
mento, o estado em que ambas as atividades sejam executadas deve ser alcançado e não mais abandonado
até o final do fluxo.
Figura 21: A execução de uma atividade/mensagem/estado implica na execução de outra
Fonte: Barros e Song (2011)
Para avaliar este tipo de relação, usa-se o seguinte comando, no qual X e Y representam compo-
nentes do fluxo. Tal comando pode ser traduzido como: em todas as atividade/estados do modelo sempre
que a atividade X for executada vai implicar que em todos os caminhos, no futuro, a atividade Y vai ser
executada. Como exemplo, pode-se pensar em um processo corporativo de compras e na validação da
seguinte regra: sempre que a compra for aprovada por um supervisor, a compra deverá ser realizada.
Caso haja um encaminhamento em que a compra não seja realizada, a resposta será negativa.
SPEC AG(atividadeX→ AF (atividadeY));
4.2.2 A execução de uma atividade/mensagem/estado implica na não execução de outra
Figura 22: A execução de uma atividade/mensagem/estado implica na não execução deoutra
Fonte: Barros e Song (2011)
Para avaliar este tipo de relação, Figura 22, utiliza-se o seguinte comando:
SPEC AG(atividadeX→ AG(!atividadeY));
Pode ser traduzido como: em todos os estados do modelo sempre que a atividade X for executada
vai implicar que em todos os caminhos, no futuro, a atividade Y não vai ser executada. Se tomado o
mesmo exemplo anterior, poderia ser verificado se sempre que o supervisor reprovar uma compra, ela
nunca será realizada. Caso haja um encaminhamento em que a compra possa ser realizada, a resposta
será negativa.
56
4.2.3 A execução de uma atividade/mensagem/estado significa a possibilidade da execuçãode outra.
Figura 23: A execução de uma atividade/mensagem/estado significa a possibilidade daexecução de outra
Fonte: Barros e Song (2011)
Para avaliar a regra representada pela Figura 23, usa-se o seguinte comando:
SPEC EF ((atividadeX→ EF(atividadeY)) & (E[!atividadeY U atividadeX]) & atividadeX &
atividadeY);
Pode ser traduzido como: se a atividade X for executada, existirá ao menos um caminho em
que no futuro a atividade Y também será, sendo que a atividade Y não pode ter sido executada antes
da atividade X. No mesmo exemplo de compras corporativas, uma regra que pode ser testada por esta
relação é a verificação se uma compra, mesmo que reprovada por uma auditoria seja concretizada. Tal
hipótese aconteceria se, por exemplo, o fluxo tiver contemplado a possibilidade de a auditoria rever o
processo e aprová-lo. Se no fluxo estiver definido que sempre que a auditoria reprovar um processo este
deverá ser cancelado, então a resposta para a regra seria negativa.
4.2.4 A execução de uma atividade/mensagem/estado depende da prévia execução de outra
Figura 24: A execução de uma atividade/mensagem/estado depende da prévia execuçãode outra
Fonte: Barros e Song (2011)
Para esta regra representada pela Figura 24, o comando completo desta avaliação será:
SPEC !EF(!atividadeX & atividadeY) & !EF(! atividadeX & !atividadeY & EX(atividadeX &
atividadeY));
57
Esta avaliação é realizada em duas etapas. Primeiro pesquisa-se se não existe um caminho em
que no futuro o estado X não é executado e o Y sim. A segunda parte pesquisa se não existe um caminho
no quais ambas as atividades são executadas ao mesmo tempo. Com as duas verificações garante-se que
a segunda atividade só é executada se a anterior também é e se elas não são executadas ao mesmo tempo.
No exemplo do processo de compras, pode-se testar se tarefas que estejam modeladas como sendo de
execução paralela, na verdade deveriam ser sequenciais. Se no fluxo for possível fazer a solicitação
de um produto e em seguida o pagamento. Porém se este pagamento for dependente de uma tarefa
sendo executada paralelamente, por exemplo, a formalização do pedido, então esta última tarefa deve ser
executada antes do pagamento. Ou seja, o pagamento não poderá ser paralelo à formalização do pedido,
somente a solicitação.
4.2.5 É possível que uma determinada atividade/mensagem/estado não seja executado
Figura 25: É possível que uma determinada atividade/mensagem/estado não seja execu-tado
Fonte: Barros e Song (2011)
Para esta regra, demonstrada pela Figura 25, usa-se o seguinte comando para avaliar:
SPEC !EG(!atividadeX );
O comando é traduzível por: existe um caminho no qual a atividade X não é executada. No
processo de compras, pode-se testar se existe a possibilidade de que a tarefa de avaliação do superior não
seja executada, por exemplo, se a compra for de valor pequeno.
4.2.6 Uma determinada atividade/mensagem/estado nunca é executado
O seguinte comando é usado para avaliar este tipo de relação, mostrado na Figura 26.
SPEC AG(!atividadeX );
Por meio do comando pesquisa-se pela validade da afirmativa de que, em todos os caminhos
possíveis, a atividade X não é executada. Em outras palavras, verificasse se o elemento pesquisado possui
grau zero de entrada, não possuindo transições que apontem para ele. A utilidade desta verificação diz
respeito mais à verificação de erros de modelagem do que a verificação de erros de lógica de negócio.
58
Figura 26: Uma determinada atividade/mensagem/estado nunca é executado
Fonte: Barros e Song (2011)
4.2.7 É sempre possível atingir o final do fluxo
Para avaliar a regra usa-se o seguinte comando:
SPEC AG(atividadeX→ AF(atividadeY));
Neste comando a atividade X é entendida como o nó inicial do fluxo abstrato e o Y o nó final
geral. Ou seja, o comando é traduzível por: sempre que o nó inicial for executado o nó final também será.
Três ocorrências são capazes de gerar uma resposta negativa para esta regra. A primeira é a inexistência
de nó final para o fluxo principal. Se por exemplo for testado um fluxo parcialmente modelado, não
será sequer possível executar essa validação por não ser possível determinar qual é o nó final. A segunda
possibilidade é a existência de caminhos com elementos desconexos, que não possibilitam que o caminho
atinja o nó final. Finalmente, a existência de ciclos sem a especificação correta de condição de interrupção
gera a possibilidade de um caminho que sempre permanece dentro do ciclo.
4.3 A Ferramenta para Automatização da Tradução e Verificação
A fim de validar a metodologia para a tradução dos diagramas de estados, atividades e sequência
para a linguagem da Verificação Simbólica de Modelos, criou-se uma ferramenta que automatiza todo
o processo, oferece um conjunto de regras para avaliar os diagramas, realiza validações de acordo com
o conjunto de regras e exibe os resultados obtidos, sendo estes positivos ou negativos. No caso de
resultados negativos um contraexemplo é exibido para justificar a resposta.
A Figura 27 apresenta uma visão geral da arquitetura da ferramenta que foi desenvolvida através
da linguagem Java. A ferramenta foi desenvolvida utilizando as bibliotecas de aplicação Java SE. A
biblioteca open source JDOM também foi utilizada. JDOM é uma biblioteca que possibilita a leitura e
gravação de arquivos no formato XML. Além desta biblioteca, foi introduzido na ferramenta o verificador
simbólico de modelos NuSMV que é responsável por executar as validações.
A ferramenta recebe como entrada o diagrama modelado no formato de arquivo XMI. O tradutor
é o responsável por percorrer o arquivo de entrada traduzindo-o para o modelo de verificação. Após a
59
tradução e juntamente com as propriedades a serem validadas (informadas pelo usuário) o diagrama é
validado através do verificador simbólico NuSMV. Concluída a execução, a interface se encarrega de
analisar a resposta obtida e exibi-la ao usuário de forma simplificada. A ferramenta possui duas interfa-
ces, a primeira interface é responsável pela tradução dos diagramas. Já segunda interface é responsável
pela verificação dos modelos. A seguir são apresentadas cada uma destas interfaces.
Figura 27: Arquitetura da ferramenta
Fonte: Elaborada pelo autor
A primeira interface, que é responsável pela tradução dos diagramas, é exibida na Figura 28.
Note que esta interface possui dois campos: Entrada e Saída. No campo Entrada o usuário informa
o arquivo XMI que deseja realizar a tradução. Já no campo Saída o usuário deve informar onde serão
gerados os arquivos traduzidos no formato da linguagem aceita pelo verificador simbólico de modelos.
Para traduzir o usuário deve acionar o comando Traduzir.
Após a tradução do diagrama o usuário poderá validá-lo. Na segunda interface, exibida na Fi-
gura 29, o usuário seleciona as duas propriedades que deseja validar e a regra que pretende aplicar nas
propriedades. Para validar o usuário deve acionar o comando Verificar. Após a validação é exibido na
caixa de texto a resposta positiva ou o contraexemplo no caso de respostas negativas.
60
Figura 28: Interface de tradução
Fonte: Elaborada pelo autor
Figura 29: Interface de verificação
Fonte: Elaborada pelo autor
61
5 ESTUDO DE CASO
Estudos de caso são coleções de informações detalhadas sobre uma determinada situação. Ge-
ralmente inclui uma pesquisa descritiva, a exploração de um tema, e conclusões sobre o contexto da
situação. Existem diferentes tipos de estudos de caso como, por exemplo, ilustrativos, exploratórios,
narrativos e exemplos críticos.
Neste trabalho o estudo de caso realizado é do tipo ilustrativo. Estudos de caso do tipo ilustrativos
são estudos descritivos que normalmente utilizam uma ou mais instâncias de um determinado evento para
descrever uma situação. Estes estudos servem para introduzir um conceito e apresentar uma visão comum
sobre o tema.
Dessa forma realiza e apresenta-se neste capítulo um estudo de caso ilustrativo a fim de demons-
trar o uso do arcabouço desenvolvido tanto no quesito das traduções quanto nas verificações realizadas
através da CTL.
5.1 Unidades de Análise
Para este estudo de caso foram utilizados diagramas da UML de dois projetos: Merci (http://
dcc.ufmg.br/~wilson/praxis) e PingIFES (http://pingifes.mec.gov.br/pingifes). O pro-
jeto Merci foi originalmente projetado e desenvolvido para ilustrar o processo Praxis. O sistema tem
como objetivo oferecer um apoio informatizado ao controle de vendas, estoque, fornecedores e estoque
de uma mercearia. Este projeto possui diversos diagramas que permitiram a realização do estudo de caso.
Os diagramas utilizados correspondem à versão 1.5 do Merci.
Já o PingIFES é um projeto realizado pelo Laboratório de Computação Científica (LCC) da Uni-
versidade Federal de Minas Gerais (UFMG) para auxiliar as equipes técnicas das Instituições Federais
de Ensino Superior (IFES) no processo de importação de dados. Este projeto tem como objetivo prin-
cipal a implantação de um processo de carga automatizada para um modelo de dados intermediário,
fornecendo dados consistentes para o processo de coleta de dados da Secretaria de Educação Supe-
rior (SESu)/Ministério da Educação (MEC). Neste estudo de caso foram utilizados os diagramas da
ferramenta pCollecta, que é uma ferramenta para a extração, transformação e carga de dados entre dois
repositórios de dados. Os diagramas utilizados correspondem à versão 1.1.2 do pCollecta.
É importante ressaltar que os projetos selecionados para o estudo de caso possuem documentação
aberta. Nesta dissertação, por limitação de espaço, somente os dados necessários foram apresentados. O
leitor interessado poderá consultar as demais informações diretamente na fonte.
62
5.2 Validações
Esta seção apresenta as avaliações que foram feitas nos sistemas apresentados. Entretanto,
destaca-se que algumas restrições são impostas nas validações de alguns modelos.
Avaliar se uma determinada atividade não será executada mais de n vezes não é possível, pelo
fato de não ter sido incluído à abordagem o controle de quantidade de execuções para cada atividade.
Propriedades do tipo soundness, como identificado por Verbeek, Aalst e Hofstede (2007), são
utilizadas para verificar se todas as atividades iniciadas são finalizadas. A verificação de tal tipo de
propriedade também não é passível de incorporação na abordagem pelo fato de não ser controlado se
uma atividade é iniciada e terminada, somente se foi executada ou não em determinado momento.
Ocorrências de deadlock, como definidas em vários trabalhos, são detectáveis pela abordagem de
maneira indireta, ao verificar se sempre o fluxo consegue atingir seu final. Caso existam ciclos sem limite
de execução, este fato indica a existência de deadlocks. Livelocks não são incorporáveis à abordagem por
não existir o controle de recursos dentro dos fluxos, somente a execução das atividades. Barros e Song
(2011) propõe sete tipos regras que serão aplicadas nesta dissertação. A seguir segue a descrição de cada
validação.
5.3 Avaliação e Resultados
Com o intuito de avaliar a capacidade do arcabouço em detectar problemas e efetivamente au-
xiliar na validação dos diagramas buscou-se obter modelagens reais, suas revisões anteriores e testá-las
para traçar uma comparação entre o que foi corrigido na prática e quais correções seriam detectáveis pelo
software. No entanto não foi possível obter tais documentos, tanto do estudo de caso, quanto de outros
diagramas para que pudessem servir como base para teste.
Todas as validações identificadas para a abordagem foram testadas em suas hipóteses de respos-
tas positivas e negativas, sendo que, no caso de respostas negativas é apresentado um contraexemplo para
justificar a resposta negativa. Privilegiaram-se testes que utilizassem o estudo de caso sem alterações,
quando isto fosse possível. Caso contrário, optou-se pela inserção de erros controlados que simulasse
tais ocorrências. Apresenta-se a seguir os resultados para os diagramas da UML abordados no trabalho
e para cada tipo de validação identificada.
5.3.1 Diagramas de Atividades
Para demonstrar as avaliações realizadas nos diagramas de atividades foram escolhidos dois
diagramas do projeto pCollecta. O primeiro diagrama de atividade é o Escalonador, representado pela
Figura 30. Este diagrama foi utilizado para modelar as atividades realizadas durante o processo de
execução das tarefas agendadas para importação de dados do projeto.
63
Figura 30: Diagrama escalonador
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
O segundo diagrama de atividade é o Exclusão de Dados, ilustrado pela Figura 31. Este diagrama
modela as atividades do sistema que fazem parte do processo de exclusão de dados dos repositórios das
IFES.
5.3.1.1 A execução de uma atividade implica na execução de outra
Tome como exemplo o diagrama de atividades Escalonador. Neste diagrama foi testada a regra
de que sempre que a atividade Ler agendamentos for executada (Figura 32), também será executada a
atividade Ler próximo agendamento na lista. Pode-se observar através da Figura 33 que a propriedade
64
Figura 31: Diagrama exclusão de dados
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
Figura 32: Escalonador: atividades em sequência
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
foi satisfeita. Tal resposta está correta, pois em todos os caminhos de execução possíveis a partir da
primeira atividade, a segunda atividade também será executada.
Em outra avaliação, analisando um objeto de decisão (Figura 34), obteve-se resposta negativa.
Ao se verificar a afirmativa de que sempre que a atividade Ler agendamentos for executada acontecerá
também a execução da atividade Todos os agendamentos da lista foram examinados, obtendo-se a res-
posta negativa.
Neste caso, tal propriedade está correta, pois existe a possibilidade da segunda atividade não ser
executada a partir da primeira, dependendo da validade da condição do elemento de decisão que verifica
se não existe próximo agendamento.
Pode-se observar na Figura 35 que em respostas negativas um contraexemplo é fornecido em um
campo específico da interface. Tal contraexemplo consiste na descrição de uma sequência de execução
possível em que o modelo viole a regra analisada.
65
Figura 33: Mensagem de sucesso
Fonte: Elaborada pelo autor
Figura 34: Escalonador: objeto de decisão
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
Figura 35: Mensagem de contraexemplo
Fonte: Elaborada pelo autor
66
Outra hipótese de obtenção de uma resposta negativa para esse tipo de validação é a própria
inexistência de caminho de execução entre os elementos analisados. Utilizando como base o diagrama
de atividade Exclusão de dados da Figura 36, pode-se notar que não existe caminho de execução possível
no qual a execução da atividadeGravar mensagem de erro implique na execução da atividade Lê próximo
registro, por exemplo. Tal hipótese ao ser validada resulta em uma resposta negativa, como esperado.
Figura 36: Exclusão de dados: caminhos distintos
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
Este tipo de validação também é afetado no caso de ciclos ininterruptos. Ao validar o diagrama
Escalonador da Figura 30, se a atividade Ler próximo agendamento da lista implica na execução da
atividade Ler próxima organização fonte de coleta, para esta validação será obtida corretamente a res-
posta negativa pelo fato de ocorrer um ciclo ininterrupto envolvendo tal fluxo. A ocorrência de um ciclo
ininterrupto resulta na existência de pelo menos um caminho em que a sequência de execução não atinge
a segunda atividade.
5.3.1.2 A execução de uma atividade implica na não execução de outra
Esta validação não é exatamente o contrário da anterior. Respostas negativas para o caso anterior
não significam necessariamente respostas positivas para o atual. Tal informação pode ser confirmada
retomando-se a segunda validação realizada anteriormente, na qual testou-se o diagrama Escalonador,
o relacionamento entre as atividades Ler agendamentos e Todos os agendamentos da lista foram exa-
minados, representado na Figura 34. Ao avaliar a afirmativa de que sempre que a primeira atividade
for executada, a segunda não será, obtêm-se novamente uma resposta negativa. A resposta se encontra
correta, pois mesmo que a segunda atividade não seja executada sempre que a primeira for, não significa
que aquela nunca será executada quando esta for.
Dessa forma, respostas negativas são obtidas quando existir alguma possibilidade da execução
das duas atividades em uma mesma sequência de execução. Para testar tal ocorrência, repetiu-se os dois
primeiros testes do caso anterior obtendo-se a resposta esperada em ambos os casos.
67
A resposta positiva para esta validação é alcançada se forem avaliados elementos em caminhos
excludentes. Caminhos excludentes são obtidos a partir de objetos de decisão que não estejam inseridos
em ciclos. Se esses estiverem em ciclos, seria possível a execução de caminhos excludentes em alguma
sequência do ciclo. O diagrama de Exclusão de dados possui caminho excludente logo após a execução
da atividade Abrir o repositório de dados (Figura 36), então testou-se na ferramenta se ao executar
a atividade Iniciar leitura dos registros no repositório implica na não execução da atividade Gravar
mensagem de erro e obteve-se a resposta positiva, como esperado.
5.3.1.3 A execução de uma atividade significa a possibilidade da execução de outra
Para esta validação, obtêm-se verdadeiro se existir ao menos uma possibilidade de que ambas
atividades possam ser executadas em uma sequência. Como consequência lógica, sempre que no primeiro
tipo de validação a resposta for positiva, nesta também será. Testou-se a hipótese que obteve tal resposta
na primeira validação e a ferramenta informou corretamente a validade da regra. Porém não é possível
concluir que, sempre que se obtiver resposta negativa para o segundo tipo de validação, será obtido a
resposta positiva neste tipo.
Por conclusão lógica, quando se compara esta validação com as anteriores, obtêm-se respostas
negativas se for obtidas respostas positivas para a segunda. Quando utilizadas as mesmas validações do
tipo anterior com as respostas apontadas acima, obteve-se respostas negativas. No entanto, respostas
negativas para o primeiro tipo não significa a obtenção de resposta negativa para este.
5.3.1.4 A execução de uma atividade depende da prévia execução de outra
Este tipo de validação pode ser considerado um tipo de detalhamento da primeira validação. Para
obter respostas positivas, não somente é necessário obter positivo para a primeira validação, mas também
é preciso que os elementos avaliados não sejam executados simultaneamente. Dessa forma, garanta-se
que uma determinada atividade só será executada se outra for executada e concluída anteriormente.
O primeiro teste realizado, entre as atividades Ler agendamentos e Ler próximo agendamento
da lista do diagrama Escalonador, foi refeito para este de tipo de validação. Foi testado se esta segunda
atividade depende da execução prévia da primeira e a ferramenta apresentou resposta positiva como
esperado.
Uma hipótese de obtenção de resposta negativa para este caso acontece quando é obtido falso
para a avaliação do primeiro tipo. Testou-se as três hipóteses que obtiveram falso como resposta para o
primeiro tipo e, em todos os casos, obteve-se falso.
Outra possibilidade para a obtenção de falso se refere ao caso em que as atividades são executa-
das simultaneamente. Isso poderia ocorrer no caso de caminhos paralelos.
68
5.3.1.5 É possível que uma determinada atividade não seja executado
Para este tipo de validação, assim como para o próximo, nos quais os elementos são avaliados
isoladamente, não é possível testar objetos de definição de condicional ou paralelismo. Tais elementos,
apesar de serem avaliados pela ferramenta e terem suas lógicas traduzidas, não são transformados em
variáveis pelo simples fato de não representarem ações passíveis de execução, mas sim definições de
lógica do processo.
Obtêm-se respostas positivas para esta validação quando o elemento analisado encontra-se em
um caminho derivado de um objeto de decisão ou após ciclos ininterruptos. Como teste desta ocorrência,
verificou-se qual seria a resposta obtida pela ferramenta para as atividades Gravar mensagem de erro,
Inicia a leitura de registros e Exclui todos os mapeamentos no diagrama de atividades Exclusão de dados,
ilustrado pela Figura 31. Obteve-se corretamente a resposta positiva para ambas, pois todas as atividades
são dependentes de uma definição de condicional.
Testou-se também se a ferramenta interpreta corretamente as regras de paralelismo, não apli-
cando a mesma lógica de objetos de condicional. Para isso utilizou-se as atividades Ler próxima orga-
nização e Executar processo de importação que estão posicionadas no diagrama de atividades Esacalo-
nador (Figura 37) logo após o objeto de paralelismo e obteve-se corretamente a resposta negativa para o
teste.
Figura 37: Escalonador: paralelismo
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
Para obtenção de resposta negativa é necessário que o elemento avaliado seja executado em todas
as hipóteses de caminho do fluxo. No diagrama de atividades Exclusão de dados, essa regra somente se
aplica a primeira atividade Abrir o repositório de dados. Todos os outros podem não ser executados seja
pela existência dos ciclos, seja pela dependência de condicionais, como pode ser observado na Figura
31.
5.3.1.6 Uma determinada atividade nunca é executado
Nesse caso, somente se o elemento avaliado estiver desconexo, é obtido verdadeiro como res-
posta. Para testar tal possibilidade foi necessário foi necessário lançar mão da inserção de erros controla-
dos. Testou-se a atividade Exclui o registro no repositório que pertence ao diagrama Exclusão de dados,
69
como mostra a Figura 38, antes e após a remoção da transição de entrada.
Figura 38: Exclusão de dados: antes e depois da remoção da transição de entrada
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
Dessa forma, o teste realizado antes da remoção de entrada a resposta dada pela ferramenta foi
negativa, por tanto existe pelo menos um caminho em que a atividade Exclui registro no repositório
será executada. Logo em seguida, foi realizada a remoção de entrada para atividade em questão e a
ferramenta deu resposta positiva, conforme esperado, pois a atividade não possui nenhuma ligação com
outra atividade do diagrama de atividades, sendo assim impossível que esta atividade seja executada.
5.3.1.7 É sempre possível atingir o final do fluxo
Para obter resposta positiva para esta validação é necessário que exista um nó final no fluxo do
diagrama e que este nó final esteja desconexo e que não haja fluxos ininterruptos no diagrama. Testado
o diagrama Exclusão de dados, Figura 31, obteve-se a resposta negativa devido ao fato deste diagrama
possuir dois nós finais, além de possuir um fluxo ininterrupto, sendo assim, se torna impossível neste
diagrama determinar em qual dos dois nós finais este fluxo do diagrama terminará.
Portanto testou-se o diagrama de atividades Emissão de nota fiscal, Figura 39, para validar se
sempre será possível atingir o final do fluxo e a ferramenta exibiu a resposta positiva, como este diagrama
não possui fluxos ininterruptos e o estado final conexo a resposta esta correta.
5.3.2 Diagrama de Estados
5.3.2.1 A execução de um estado implica na execução do outro
Para validar esta regra testou-se no diagrama de estadosModos de operação, Figura 40, se sem-
pre que a transição Fechar caixa for executada implica na execução do estadoModo de gestão, a resposta
obtida pela ferramenta foi de que tal regra é verdadeira. Tal resposta esta correta, pois a transição em
70
Figura 39: Diagrama emissão de nota fiscal
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
questão realiza uma ligação direta ao estado, portanto sempre que a transição for executada o estado
também será executado.
Figura 40: Diagrama modos de operação
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
Já no diagrama de estados Agendamento, representado pela Figura 41, verificou-se a execução
da transição Criar processo implica na execução do estado Finalizado. Para esta validação foi obtida a
71
resposta negativa, devido ao fato de haver no diagrama de estados um ciclo ininterrupto envolvendo tal
fluxo. Outra hipótese de obtenção resposta negativa para esse tipo de validação é a própria inexistência
de um caminho de execução entre os elementos analisados.
Figura 41: Diagrama agendamento
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
5.3.2.2 A execução de um estado implica na não execução de outro
Como dito anteriormente essa validação não é exatamente o contrário da validação anterior. Tal
afirmação pode ser confirmada retomando-se a segunda validação realizada na subseção anterior, na
qual testou-se o relacionamento entre a transição Criar processo e o estado Finalizado do diagrama de
estado Agendamento, representado na Figura 41. Ao testar a afirmativa de que sempre que a transição
for executada, o estado não será, obtém-se novamente uma resposta negativa. A resposta se encontra
correta, pois mesmo que estado não seja executado sempre que a transição é executada, isso não significa
que ele nunca será executado quando a transição for executada.
Para obter resposta positiva para esta validação, se forem avaliados elementos em caminhos
excludentes. No diagrama de estado Agendamento (Figura 41), não existe estado que possua tal carac-
terística. Os estados Aguardando, Em execução, Suspenso e Finalizado não podem ser usados para este
teste, pois estão envolvidos em ciclos.
5.3.2.3 A execução de um estado significa a possibilidade da execução de outro
Sempre que no primeiro tipo de validação a resposta for positiva, nesta também será. Testou-se a
hipótese que obteve tal resposta na primeira validação e a ferramenta informou corretamente a validade
da regra. Porém não é possível concluir que, sempre que se obtiver resposta negativa para o segundo tipo
de validação, será obtido à resposta positiva neste tipo.
72
Ainda por conclusão lógica, quando se compara esta validação com as anteriores, obtêm-se res-
postas negativas se for obtidas resposta positivas para a segunda. Quando utilizadas as mesmas validações
do tipo anterior com as respostas apontada acima, obteve-se respostas negativas. No entanto, respostas
negativas para o primeiro tipo não significa a obtenção de respostas negativas para este.
5.3.2.4 A execução de um estado depende da prévia execução de outro
O primeiro teste realizado, entre a transação Abrir Caixa e o estadoModo de vendas, do diagrama
de estados Modos de operação, representado na Figura 40. Foi testado se o estado Modo de vendas
depende da execução prévia da transição Abrir caixa. A ferramenta obteve resposta positiva, como
esperado. Como o único caminho possível de chegar ao estadoModo de vendas é pela transição avaliada,
a resposta apresentada esta correta.
No caso de resposta negativa para este caso se dá quando é obtido falso para a avaliação do
primeiro tipo. Logo, testou-se a validação que obteve resposta negativa na primeira avaliação do dia-
grama de estado Agendamento. O teste realizado verificando-se o estado Finalizado depende de previa
execução da transição Criar processo, apresentou resposta negativa da ferramenta, conforme esperado.
5.3.2.5 É possível que um determinado estado não seja executado
Obtêm-se respostas positivas para esta validação quando o elemento analisado encontra-se em
um caminho derivado de um objeto de decisão ou após ciclos ininterruptos. Como teste desta ocorrência,
verificou-se qual seria a resposta obtida pela ferramenta para o estado Suspenso do diagrama de estado
Agendamento (Figura 41). Obteve-se corretamente a resposta positiva, pois o estado faz parte de um
ciclo ininterrupto.
Em seguida, foi realizada a verificação no diagrama de estado Modos de operação para avaliar
se é possível o estado Modo de gestão não seja executado, a ferramenta apresentou a resposta negativa.
Tal avaliação esta correta devido ao fato do estado ser executado em todas as hipóteses de caminho do
fluxo do diagrama.
5.3.2.6 Um determinado estado nunca é executado
Nesta validação verificou o diagrama de estado Agendamento e foi necessário introduzir erros
controlados. Testou-se o estado Suspenso nunca é executado antes e após a remoção da transição de
entrada. Antes da remoção a resposta obtida pela ferramenta foi negativa, portanto existe pelo menos
um caminho onde o fluxo do diagrama leva ao estado Suspenso. Como a remoção da transição Suspende
processo o diagrama de estados ficou modelado conforme a Figura 42. Dessa forma foi realizou-se
novamente a verificação se o estado Suspenso nunca é executado e obteve-se resposta positiva. Tal
afirmação esta correta, pois na existe nenhuma transição ligando ao estado avaliado.
73
Figura 42: Diagrama agendamento alterado
Fonte: Criado pelo autor com dados extraídos do LCC/CENAPAD
5.3.2.7 É sempre possível atingir o final do fluxo
Testou-se no diagrama de estado Agendamento sempre é possível atingir o final do fluxo, a
ferramenta apresentou resposta negativa. Tal resposta esta correta pelo fato do fluxo do diagrama possuir
ciclos ininterruptos. Para obter resposta positiva nesse caso é necessário alterar o diagrama de tal forma
que ele não possua mais ciclos ininterruptos.
5.3.3 Diagrama de Sequência
5.3.3.1 A execução de uma mensagem implica na execução de outra
Testou-se o diagrama de sequência Inserção de novo item de venda, Figura 43, verificando se
a execução da mensagem Incluir item implica na execução da mensagem Inserir novo item, a resposta
obtida pela ferramenta foi positiva. Tal resposta esta correta, pois logo na sequência da execução primeira
mensagem a segunda mensagem é executada.
Para outra validação, executável no mesmo diagrama, obteve-se resposta negativa. Validou-se
a mensagem Totalizar implica na execução da atividade Incluir item, conforme esperado a resposta da
ferramenta foi negativa. Tal validação esta correta, pois a atividade Totalizar somente é executada uma
vez que a atividade Incluir item já foi executada.
5.3.3.2 A execução de uma mensagem significa a possibilidade da execução de outra
Para esta validação respostas negativas são obtidas para atividades que são executadas em uma
mesma sequência de execução. Como o diagrama de sequência tem como principal objetivo descrever a
sequência de execução das mensagens, para todas as mensagens são obtidas respostas negativas.
74
Figura 43: Diagrama inserção de novo item
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
5.3.3.3 A execução de uma mensagem depende da prévia execução de outra
Como descrito anteriormente essa validação pode ser considerada como um detalhamento da
primeira validação. O primeiro teste realizado, entre as mensagens Inserir novo item e Recuperar foi
realizado, verificando-se se a execução da primeira mensagem significa a possibilidade da execução da
segunda mensagem. Na ferramenta obteve-se resposta positiva, como esperado, pois as mensagens estão
em sequência.
Respostas negativas que são obtidas para a primeira avaliação também ocorrem para esta vali-
dação. Testaram-se as hipóteses que obtiveram falso como resposta para o primeiro tipo e, em todos os
casos, obteve-se falso.
Outra possibilidade para obtenção de falso se refere ao caso em que as atividades são executadas
simultaneamente. Nesse caso, testou-se no diagrama de sequência, se a mensagem Atribuir mercadoria
significa a execução da mensagem Atribuir quantidade, ambas as mensagens fazem parte de um para-
lelismo (Figura 44), e a resposta obtida pela ferramenta foi negativa. Isto ocorre devido ao fato das
mensagens executarem de forma paralela.
75
Figura 44: Inserção de novo item: paralelismo
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
5.3.3.4 É possível que uma determinada mensagem não seja executado
Através desta validação é possível verificar as condicionais presentes no diagrama de sequência.
Avaliou-se, no diagrama de sequência Inserção de Novo Item, a condicional Controlar de Venda - Novo
(Figura 45) presente para execução da mensagem Inserir Item de Venda. Testou-se é possível que a
mensagem Inserir Item de Venda não seja executada, e a ferramenta exibiu a mensagem verdadeira. Tal
avaliação esta correta, pois a mensagem depende da satisfação de uma condicional antes de sua execução.
Figura 45: Inserção de novo item: condicional
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
5.3.4 Considerações Finais
Neste Capítulo foram apresentados apenas alguns dos diagramas utilizados no estudo de caso
para validação da metodologia e arcabouço. A Tabela 46 apresenta um resumo de todos os testes re-
alizados e os resultados obtidos. As linhas marcadas em cinza correspondem aos testes previamente
apresentados, as demais correspondem aos testes apresentados em anexo.
Nesta tabela para cada validação (Coluna Validações) foi realizado pelo menos um teste com
cada tipo de diagrama (Coluna Diagrama). As colunas Nome do Diagrama e Projeto apresentam, res-
pectivamente, o nome do diagrama utilizado na validação na qual projeto o mesmo pertence. As colunas
Primeiro Elemento e Segundo Elemento apresentam os elementos do diagrama em questão envolvidos na
76
Figura 46: Quadro de resultados dos testes
Fonte: Elaborada pelo autor
77
validação. Por fim, o resultado obtido em cada umas das validações é apresentado (Coluna Resultado).
O estudo de caso realizado apresenta algumas limitações por ser do tipo ilustrativo. O motivo
deste tipo de estudo ter sido realizado se deve por dois fatores. O primeiro está relacionado ao fato de
que nem todos os projetos fazerem o uso de diagramas para a modelagem de sistemas. O segundo está
relacionado à dificuldade em encontrar empresas que permitissem uma aplicação real da abordagem pos-
sibilitando uma análise sobre os seus custos e benefícios. Para tal tipo de análise haveria a necessidade
de obter informações não só da modelagem do sistema, mas de toda a documentação gerada pelo pro-
cesso. Por questões de segurança as empresas optam por não disponibilizar tais informações, pois não
gostariam de tê-las divulgadas.
Por estes motivos, o estudo de caso realizado permitiu descrever apenas como as validações
podem ser realizadas apresentando a viabilidade da abordagem, mas não permite avaliar os reais custos
e benefícios da mesma.
Entretanto, um benefício da abordagem é a utilização de lógica formal para que o usuário re-
alize validações detectando defeitos de um sistema antecipadamente (i.e., logo no início do processo)
a um custo relativamente mais baixo (i.e., sem a necessidade do usuário entender de lógica formal).
No próximo Capítulo apresenta-se a conclusão desta dissertação, assim com as sugestões de trabalhos
futuros.
78
6 CONCLUSÕES
O tema da verificação de diagramas da UML vem adquirindo importância na última década e
se mostrado eficaz na resolução antecipada de inconsistências que podem representar custos de solução
crescentes ao longo dos projetos de desenvolvimento e ao longo da vida útil dos softwares. Detectar erros
nesse estágio também representa oportunidades de revisão e otimização das modelagens de software,
assim como a redução de riscos em casos de processos críticos. A técnica de Model Checking se mostra
adequada para o propósito de validação destes diagramas, conforme pode ser observado neste e em outros
trabalhos relacionados.
O presente trabalho apresenta um arcabouço e uma ferramenta para a realização de verificações
nos fluxos de execução dos diagramas de atividades, estados e sequência, podendo ser automatizado
por meio de uma interface que abstrai grande parte da complexidade do processo, aumentando assim a
aplicabilidade da técnica. Tendo como público-alvo os profissionais especialistas em engenharia de soft-
ware, foi importante que essa metodologia não exigisse conhecimentos específicos de técnicas formais.
Também é importante que não se exija a adaptação das modelagens já existentes e que se utilize como
base a UML, que é uma linguagem difundida e adequada aos propósitos do software. Nesse sentido,
mesmo com objetivos próximos aos de outras pesquisas, foi possível inovar ao trazer vários aspectos
conjugados que resultou em uma ferramenta que estará disponível em código aberto.
Também se destaca a identificação dos casos de tradução, representando as possibilidades de va-
riação de comportamento da execução de fluxos de modelagem e as validações possíveis. Para o objetivo
do presente trabalho, estes se mostraram suficientes e adequados. Toda a lógica de tradução apresen-
tada pela abordagem foi considerada no desenvolvimento do software, demonstrando a viabilidade e
capacidade de automatização.
Por meio dos testes realizados e da validação dos estudos de caso foi possível testar a eficácia
do arcabouço e o alcance dos objetivos propostos. Foi possível não somente detectar os erros propo-
sitalmente simulados nos diagramas, mas também a verificação de adequação entre modelagens e suas
respectivas alterações/traduções para fins de organização e automatização.
A maior ressalva quanto à aplicabilidade do arcabouço se refere à possibilidade de execução
infinita de ciclos. Não se impôs um padrão de modelagem específico para a abordagem. Outra limitação
é a inviabilidade de incorporação de outras validações usando a estrutura proposta, como descrito na
seção 5.2. Também existe a limitação de restrição quanto ao número de relações entre os elementos dos
diagramas na ferramenta. Esta decorre da própria criação da interface, voltada para simplificar o uso
79
pelos usuários não especialistas. Não são necessários conhecimentos de Lógica Temporal e Verificação
Simbólica de Modelos para obter a validação das regras de execução de fluxos dos diagramas, o que se
mostra como um dos benefícios da abordagem.
6.1 Trabalhos Futuros
Durante o desenvolvimento desta pesquisa, foram identificadas algumas questões que podem ser
consideradas a fim de dar continuidade a este trabalho. Algumas sugestões de trabalhos futuros são:
a) Incluir a tradução de outros elementos dos diagramas, a fim de suprir as limitações identificadas
na seção 5.2;
b) Realizar tradução de outros diagramas da UML, tais como diagrama de classes e caso de uso para
a Verificação Simbólica de Modelos;
c) Aplicar a abordagem em um estudo de caso real;
d) Desenvolver uma metodologia para validar a equivalência de diagramas da UML;
e) Transformar a ferramenta em um plugin para os ambientes de modelagem de diagramas;
f) Interpretar os resultados de validação, mais precisamente os contraexemplos.
80
REFERÊNCIAS
BARROS, C. Verificação Automatizada de Regras de Sequenciamento de Execução em Workflows.PUC MG, 2010, Dissertação (Mestrado) - Pontifícia Universidade Católica de Minas Gerais, MinasGerais. Disponível em: HTTP://www.biblioteca.pucminas.br/teses/Informatica BarrosCM 1.pdf.Acesso em 05 maio 2011.
BASILI, V. R.; PERRICONE, B. T. Software errors and complexity: an empirical investigation.Communications of the ACM, v.27, p.42–52, Janeiro, 1984.
BEATO, M. E. et al. UML Automatic Verification Tool with Formal Methods. Electronic Notes inTheoretical Computer Science, v.127, p.3–16, Abril, 2005.
BELL, R. M.; OSTRAND, T. J.; WEYUKER, E. J. Looking for bugs in all the right places. In:INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, 2006. Proceedingsof ISSTA. Maine: ACM, 2006. p.61–72.
BHADURI, P.; RAMESH, S. Model checking of statechart models: survey and research directions.ArXiv Computer Science e Prints, p.1–41, Julho, 2004.
BIERE, A. et al. Symbolic Model checking without BDDs. In: INTERNATIONAL CONFERENCEON TOOLS AND ALGORITHMS FOR CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1999.Proceedings TACAS. Cleveland: Carnegie Mellon University, 1999. p.193–207.
BLACKBURN, P. Nominal Tense Logic.Notre D. Journal of Formal Logic, v.34, p.56–83, Maio, 1993.
BOOCH, G.; RUMBAUGH, J.; JACOBSON, I. The unified modeling language user guide. Redwood:Addison Wesley, 2005.
BRYANT, R. E. Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions onComputers, v.35, p.677–691, Augusto, 1986.
CAVADA, R. et al. NuSMV 2.5 User Manual. 2011. Disponível em:<http://nusmv.fbk.eu/NuSMV/userman/v25/nusmv.pdf>. Acesso em 01 de dez. 2011.
CHOPPY, C.; KLAI, K.; ZIDANI, H. Formal verification of UML state diagrams: a petri net basedapproach. SIGSOFT Software Engineering Notes, v.36, p.1–8, Janeiro, 2011.
CIMATTI, A. et al. NUSMV: a new Symbolic model verifier. Computer Aided Verification, v.1633, n.4, p.495–499, 1999.
81
CLARKE, E. M. et al. Efficient generation of counterexamples and witnesses in symbolic modelchecking. In: ACM/IEEE DESIGN AUTOMATION CONFERENCE, 32, 1995. Proceedings ofDAC’95. San Francisco: ACM/IEEE, 1995. p.427–432.
CLARKE, E. M.; GRUMBERG, O.; PELED, D. A. Model Checking. Cambridge, Massachusetts: TheMIT Press, 1999.
CLARKE, E. M.; LERDA, F. Model Checking: Software and Beyond. Journal of Universal ComputerScience, v.13, p.639–649, 2007.
DUBROVIN, J.; JUNTTILA, T. Symbolic model checking of hierarchical UML state machines.In: INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEMDESIGN, 8, 2008. Proceedings of ACSD ’08. IEEE, 2008. p. 108–117.
ESHUIS, R. Symbolic model checking of UML activity diagrams. The Transactions on SoftwareEngineering and Methodology, v.15, p.1–38, 2006.
FENTON, N.; NEIL, M. A critique of software defect prediction models. IEEE Transactions onSoftware Engineering, v.25, p.675–689, 1999.
FERNANDES, F.; ALAN, M. Um arcabouço para verificação automática de modelos UML. In:CONGRESSO BRASILEIRO DE SOFTWARE: TEORIA E PRÁTICA, 2011, São Paulo. CBSoft2011. São Paulo: 2011. p. 1–7.
FERNANDES, F.; ALAN, M. Verification of UML behavioral diagrams using symbolic modelchecking. In: INTERNATIONAL CONFERENCE APPLIED COMPUTING, 2011, Rio de Janeiro.Proceedings of the IADIS. Rio de Janeiro, 2011.
PAULA FILHO, W. P. Processo Praxis 3.0. Belo Horizonte: UFMG, 2008. Disponível em:<http://homepages.dcc.ufmg.br/wilson/praxis/>. Acesso em 01 de dez. 2011.
FOWLER, M. UML Distilled: a brief guide to the standard object modeling language. 3rd ed. Boston:Addison Wesley, 2003.
FRASER, G.; WOTAWA, F.; AMMANN, P. E. Testing with model checkers: a survey. SoftwareTesting, Verification and Reliability, v.19, p.215–261, Setembro, 2009.
GRAHAM, D. et al. Foundations of software Testing: ISTQB certification. Derby: Int. ThomsonBusiness, 2008.
OBJECT MANAGEMENT GROUP. M. UML 2.3 Superstructure Specification. 2010. Disponívelem: <http://www.omg.org/spec/UML/2.3/>. Acesso em 01 de dez. 2011.
82
OBJECT MANAGEMENT GROUP. OMG MOF 2 XMI Mapping Specification. 2011. Disponívelem: <http://www.omg.org/spec/XMI/2.4.1/PDF>. Acesso em 01 de dez. 2011.
HAN, T.; KATOEN, J. P.; BERTEUN, D. Counterexample Generation in Probabilistic Model Checking.IEEE Transactions on Software Engineering, v.35, p.241–257, Abril, 2009.
KANER, C.; FALK, J. L.; NGUYEN, H. Q. Testing computer software. New York: John Wiley &Sons, 1999.
KNAPP, A.; WUTTKE, J. Model checking of UML 2.0 interactions. In: INTERNATIONALCONFERENCE ON MODELS IN SOFTWARE ENGINEERING, 2006. Proceedings of ModelsWorkshops’ 2006. Berlin: Springer-Verlag, 2006. p.42–51.
LIEBERMAN, B. A. The art of software modeling. Boca Raton: Auerbach, 2006.
LILIUS, J.; PALTOR, I. vUML: a tool for verifying UML models. In: IEEE INTERNATIONALCONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, 14, 1999. Proceedings of theASE’99. Cocoa Beach: IEEE Computing Society, 1999. p.255–258.
LOMUSCIO, A.; PECHEUR, C.; RAIMONDI, F. Automatic verification of knowledge and timewith NuSMV. In: INTERNATIONAL JOURNAL OF COMPUTER APPLICATIONS, 20, 2007.Proceedings of the IJCAI. Menlo Park: AAAI Press, 2007. p.1384–1389.
LUDEWIG, J. Models in software engineering: an introduction. Software and Systems Modeling, v.2,n.1, p.5–14, 2003.
LUTZ, C.; WOLTER, F.; ZAKHARYASHEV, M. Temporal Description Logics: A Survey. In:INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, 15,2008. Proceedings of the TIME ’08. Montreal: IEEE Computing Society, 2008. p.3–14.
MCMILLAN, K. L. Symbolic Model Checking. Norwell: Kluwer Academic Publishers, 1993.
MOKHATI, F.; GAGNON, P.; BADRI, M. Verifying UML Diagrams with Model Checking:A Rewriting Logic Based Approach. In: INTERNATIONAL CONFERENCE ON QUALITYSOFTWARE, 17, 2007. Proceedings of the QSIC ’07. Portland: IEEE Computing Society, 2007.p.356–362.
MULLER, P. A. et al. Modeling modeling modeling. Software and Systems Modeling, p.1–13,Agosto, 2010.
NUSMV. NuSMV Examples. 2011. Disponível em:<http://nusmv.fbk.eu/NuSMV/userman/v20/nusmv 2.html>. Acesso em 01 de jan. 2011.
83
OSTRAND, T.; WEYUKER, E.; BELL, R. Predicting the location and number of faults in largesoftware systems. IEEE Transactions on Software Engineering, v.31, n.4, p.340–355, Abril, 2005.
OSTRAND, T. J.; WEYUKER, E. J.; BELL, R. M. Where the bugs are. In: ACM SIGSOFTINTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, 2004. Proceedingsof the ISSTA ’04. Boston: ACM, 2004. p.86–96.
PENDER, T. UML Bible. New York: Wiley, 2003.
PRESSMAN, R. S. Software Engineering: A Practitioners Approach. 7th ed. New York: McGraw HillScience/Engineering/Math, 2009.
SARGENT, R. G. Verification and validation of simulation models. In: THE WINTER SIMULATIONCONFERENCE, 2007. Proceedings of the WSC ’07. Washington: IEEE Computing Society, 2007.p.124–137.
SEGALL, I.; TZOREF BRILL, R.; FARCHI, E. Using binary decision diagrams for combinatorial testdesign. In: INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, 2011.Proceedings of the ISSTA ’11. Toronto: ACM, 2011. p.254–264.
SEIDEWITZ, E. What models mean. IEEE Software, v.20, n.5, p.26–32, Outubro, 2003.
SELIC, B. Tutorial: an overview of UML 2. In: INTERNATIONAL CONFERENCE ON SOFTWAREENGINEERING, 26, 2004. Proceedings of the ICSE’04. Los Alamitos: IEEE Computer Society,2004, p.741–742, 2004.
SOEKEN, M. et al. Verifying UML/OCL models using Boolean satisfiability. In: THE CONFERENCEON DESIGN, AUTOMATION AND TEST IN EUROPE, 2010. Proceedings of the DATE ’10.Dresden: European Design and Automation Association, 2010. p.1341–1344.
SOMMERVILLE, I. Software Engineering. 7th ed. Boston: Pearson Addison Wesley, 2004.
VERBEEK, H.; AALST, W. van der; HOFSTEDE, A. ter. Verifying Workflows with CancellationRegions and OR joins: An Approach Based on Relaxed Soundness and Invariants. The ComputerJournal, v.50, n.3, p.294–314, 2007.
XU, D.; MIAO, H.; PHILBERT, N. Model Checking UML Activity Diagrams in FDR. In: IEEE/ACISINTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE, 8, 2009.Proceedings of the ICIS ’09. Shanghai: IEEE Computer Society, 2009. p.1035–1040.
Y., K.; ROZIER. Linear Temporal Logic Symbolic Model Checking. Computer Science Review, v.5,n.2, p.163–203, Maio, 2011.
84
ANEXO A -- DIAGRAMAS
Figura 1 - Alteração de dados de fornecedor
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
85
Figura 2 - Atualização do estoque
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
86
Figura 3 - Emissão de relatório de fornecedores
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
Figura 4 - Exclusão de fornecedor
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
87
Figura 5 - Inclusão de novo fornecedor
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
88
Figura 6 - Inclusão de novo usuário
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
Figura 7 - Seleção e impressão dos relatórios
Fonte: Criado pelo autor com dados extraídos do Filho (2011)
89
ANEXO B -- LINGUAGEM SMV
Quadro 1: Código SMV para o Diagrama Escalonador.
1 MODULE main
2 VAR
3 i n i c i a l : boo l e an ;
4 l e r a g endamen t o s : boo l e an ;
5 l e r p r o x imo a g e n d amen t o n a l i s t a : boo l e an ;
6 agendamen to l i do : boo l e an ;
7 t o d o s o s a g e nd amen t o s d a l i s t a f o r amex am i n ado s : boo l e an ;
8 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s : boo l e an ;
9 l e r l i s t a d e o r g a n i z a c o e s f o n t e d a c o l e t a : boo l e an ;
10 l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a : boo l e an ;
11 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s : boo l e an ;
12 t o d a s a s o r g a n i z a c o e s f o n t e s j a f o r am e x am i n a d a s : boo l e an ;
13 e x e c u t a r p r o c e s s o d e imp o r t a c a o p a r a a o r g a n i z a c a o f o n t e : boo l e an ;
14 f i n a l 0 2 : boo l e an ;
15 e x e c u t a r o p r o c e s s o d e impo r t a c a o : boo l e an ;
16 f i n a l 0 1 : boo l e an ;
17 p r e p a r a r e x e c u c a o : boo l e an ;
18 p r e p a r a r n o v a l i n h a : boo l e an ;
19 ASSIGN
20 i n i t ( i n i c i a l ) := TRUE;
21 i n i t ( l e r a g endamen t o s ) := FALSE ;
22 i n i t ( l e r p r o x imo a g e n d amen t o n a l i s t a ) := FALSE ;
23 i n i t ( agendamen to l i do ) := FALSE ;
24 i n i t ( t o d o s o s a g e nd amen t o s d a l i s t a f o r amex am i n ado s ) := FALSE ;
25 i n i t ( e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s ) := FALSE ;
26 i n i t ( l e r l i s t a d e o r g a n i z a c o e s f o n t e d a c o l e t a ) := FALSE ;
27 i n i t ( l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a ) := FALSE ;
28 i n i t ( e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s ) := FALSE ;
29 i n i t ( t o d a s a s o r g a n i z a c o e s f o n t e s j a f o r am e x am i n a d a s ) := FALSE ;
30 i n i t ( e x e c u t a r p r o c e s s o d e imp o r t a c a o p a r a a o r g a n i z a c a o f o n t e ) := FALSE ;
31 i n i t ( f i n a l 0 2 ) := FALSE ;
32 i n i t ( e x e c u t a r o p r o c e s s o d e impo r t a c a o ) := FALSE ;
90
33 i n i t ( f i n a l 0 1 ) := FALSE ;
34 i n i t ( p r e p a r a r e x e c u c a o ) := FALSE ;
35 i n i t ( p r e p a r a r n o v a l i n h a ) := FALSE ;
36 nex t ( l e r a g endamen t o s ) := case
37 l e r a g endamen t o s = TRUE : TRUE;
38 l e r a g endamen t o s = FALSE & todo s o s a g e nd amen t o s d a l i s t a f o r amex am i n ado s =
TRUE & i n i c i a l = TRUE : TRUE;
39 TRUE : FALSE ;
40 e s a c ;
41 nex t ( l e r p r o x imo a g e n d amen t o n a l i s t a ) := case
42 l e r p r o x imo a g e n d amen t o n a l i s t a = TRUE : TRUE;
43 l e r p r o x imo a g e n d amen t o n a l i s t a = FALSE & le r a g endamen t o s = TRUE &
t o d a s a s o r g a n i z a c o e s f o n t e s j a f o r am e x am i n a d a s = TRUE & n u l l = TRUE &
n u l l = TRUE : TRUE;
44 TRUE : FALSE ;
45 e s a c ;
46 nex t ( agendamen to l i do ) := case
47 agendamen to l i do = TRUE : TRUE;
48 l e r p r o x imo a g e n d amen t o n a l i s t a = TRUE &
todo s o s a g e nd amen t o s d a l i s t a f o r amex am i n ado s = TRUE : FALSE ;
49 l e r p r o x imo a g e n d amen t o n a l i s t a = TRUE : {FALSE , TRUE} ;
50 TRUE : FALSE ;
51 e s a c ;
52 nex t ( t o d o s o s a g e nd amen t o s d a l i s t a f o r amex am i n ado s ) := case
53 t o d o s o s a g e nd amen t o s d a l i s t a f o r amex am i n ado s = TRUE : TRUE;
54 l e r p r o x imo a g e n d amen t o n a l i s t a = TRUE & ( agendamen to l i do = TRUE | n ex t (
agendamen to l i do = TRUE) ) : FALSE ;
55 l e r p r o x imo a g e n d amen t o n a l i s t a = TRUE & agendamen to l i do = FALSE : TRUE;
56 TRUE : FALSE ;
57 e s a c ;
58 nex t ( e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s ) := case
59 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE : TRUE;
60 agendamen to l i do = TRUE & l e r l i s t a d e o r g a n i z a c o e s f o n t e d a c o l e t a = TRUE :
FALSE ;
61 agendamen to l i do = TRUE : {FALSE , TRUE} ;
62 TRUE : FALSE ;
63 e s a c ;
64 nex t ( l e r l i s t a d e o r g a n i z a c o e s f o n t e d a c o l e t a ) := case
65 l e r l i s t a d e o r g a n i z a c o e s f o n t e d a c o l e t a = TRUE : TRUE;
91
66 agendamen to l i do = TRUE & ( e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s =
TRUE | nex t ( e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE) ) :
FALSE ;
67 agendamen to l i do = TRUE & e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s =
FALSE : TRUE;
68 TRUE : FALSE ;
69 e s a c ;
70 nex t ( l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a ) := case
71 l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = TRUE : TRUE;
72 l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = FALSE &
l e r l i s t a d e o r g a n i z a c o e s f o n t e d a c o l e t a = TRUE & n u l l = TRUE & n u l l =
TRUE : TRUE;
73 TRUE : FALSE ;
74 e s a c ;
75 nex t ( e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s ) := case
76 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE : TRUE;
77 l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = TRUE &
t o d a s a s o r g a n i z a c o e s f o n t e s j a f o r am e x am i n a d a s = TRUE : FALSE ;
78 l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = TRUE : {FALSE , TRUE} ;
79 TRUE : FALSE ;
80 e s a c ;
81 nex t ( t o d a s a s o r g a n i z a c o e s f o n t e s j a f o r am e x am i n a d a s ) := case
82 t o d a s a s o r g a n i z a c o e s f o n t e s j a f o r am e x am i n a d a s = TRUE : TRUE;
83 l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = TRUE & (
e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE | nex t (
e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE) ) : FALSE ;
84 l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = TRUE &
e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = FALSE : TRUE;
85 TRUE : FALSE ;
86 e s a c ;
87 nex t ( l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a ) := case
88 l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = TRUE : TRUE;
89 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE & p r e p a r a r e x e c u c a o =
TRUE : FALSE ;
90 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE : {FALSE , TRUE} ;
91 TRUE : FALSE ;
92 e s a c ;
93 nex t ( p r e p a r a r e x e c u c a o ) := case
94 p r e p a r a r e x e c u c a o = TRUE : TRUE;
92
95 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE & (
l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = TRUE | n ex t (
l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = TRUE) ) : FALSE ;
96 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE &
l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a = FALSE : TRUE;
97 TRUE : FALSE ;
98 e s a c ;
99 nex t ( e x e c u t a r p r o c e s s o d e imp o r t a c a o p a r a a o r g a n i z a c a o f o n t e ) := case
100 p r e p a r a r e x e c u c a o = TRUE : TRUE;
101 TRUE : FALSE ;
102 e s a c ;
103 nex t ( l e r p r o x im a o r g a n i z a c a o f o n t e d a c o l e t a ) := case
104 p r e p a r a r e x e c u c a o = 1 : 1 ;
105 TRUE : FALSE ;
106 e s a c ;
107 nex t ( f i n a l 0 2 ) := case
108 f i n a l 0 2 = TRUE : TRUE;
109 e x e c u t a r p r o c e s s o d e imp o r t a c a o p a r a a o r g a n i z a c a o f o n t e = TRUE : TRUE;
110 TRUE : FALSE ;
111 e s a c ;
112 nex t ( l e r p r o x imo a g e n d amen t o n a l i s t a ) := case
113 l e r p r o x imo a g e n d amen t o n a l i s t a = TRUE : TRUE;
114 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE & p r e p a r a r n o v a l i n h a =
TRUE : FALSE ;
115 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE : {FALSE , TRUE} ;
116 TRUE : FALSE ;
117 e s a c ;
118 nex t ( p r e p a r a r n o v a l i n h a ) := case
119 p r e p a r a r n o v a l i n h a = TRUE : TRUE;
120 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE & (
l e r p r o x imo a g e n d amen t o n a l i s t a = TRUE | nex t (
l e r p r o x imo a g e n d amen t o n a l i s t a = TRUE) ) : FALSE ;
121 e x am i n a r l i s t a d e l i n h a s d e e x e c u c a o d e p r o c e s s o s = TRUE &
l e r p r o x imo a g e n d amen t o n a l i s t a = FALSE : TRUE;
122 TRUE : FALSE ;
123 e s a c ;
124 nex t ( e x e c u t a r o p r o c e s s o d e impo r t a c a o ) := case
125 p r e p a r a r n o v a l i n h a = TRUE : TRUE;
126 TRUE : FALSE ;
93
127 e s a c ;
128 nex t ( l e r p r o x imo a g e n d amen t o n a l i s t a ) := case
129 p r e p a r a r n o v a l i n h a = 1 : 1 ;
130 TRUE : FALSE ;
131 e s a c ;
132 nex t ( f i n a l 0 1 ) := case
133 f i n a l 0 1 = TRUE : TRUE;
134 e x e c u t a r o p r o c e s s o d e impo r t a c a o = TRUE : TRUE;
135 TRUE : FALSE ;
136 e s a c ;
Quadro 2: Código SMV para o Diagrama Exclusão de dados.
1 MODULE main
2 VAR
3 i n i c i a l : boo l e an ;
4 a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o : boo l e an ;
5 g rava rmensagemdee r rono log : boo l e an ;
6 f i n a l 0 1 : boo l e an ;
7 i n i c i a l e i t u r a d e r e g i s t r o s : boo l e an ;
8 l e p r o x im o r e g i s t r o : boo l e an ;
9 exc l u i t odo so smapeamen t o s : boo l e an ;
10 e x c l u i o r e g i s t r o n o r e p o s i t o r i o : boo l e an ;
11 t o d o s o s r e g i s t r o s j a f o r am e x c l u i d o s : boo l e an ;
12 gravamensagemdesucesso : boo l e an ;
13 f e c h a r o r e p o s i t o r i o d e d a d o s : boo l e an ;
14 f i n a l 0 2 : boo l e an ;
15 ASSIGN
16 i n i t ( i n i c i a l ) := TRUE;
17 i n i t ( a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o ) := FALSE ;
18 i n i t ( g r ava rmensagemdee r rono log ) := FALSE ;
19 i n i t ( f i n a l 0 1 ) := FALSE ;
20 i n i t ( i n i c i a l e i t u r a d e r e g i s t r o s ) := FALSE ;
21 i n i t ( l e p r o x im o r e g i s t r o ) := FALSE ;
22 i n i t ( e x c l u i t odo so smapeamen t o s ) := FALSE ;
23 i n i t ( e x c l u i o r e g i s t r o n o r e p o s i t o r i o ) := FALSE ;
24 i n i t ( t o d o s o s r e g i s t r o s j a f o r am e x c l u i d o s ) := FALSE ;
25 i n i t ( g ravamensagemdesucesso ) := FALSE ;
26 i n i t ( f e c h a r o r e p o s i t o r i o d e d a d o s ) := FALSE ;
94
27 i n i t ( f i n a l 0 2 ) := FALSE ;
28 nex t ( a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o ) := case
29 a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o = TRUE : TRUE;
30 a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o = FALSE & i n i c i a l = TRUE : TRUE;
31 TRUE : FALSE ;
32 e s a c ;
33 nex t ( f i n a l 0 1 ) := case
34 f i n a l 0 1 = TRUE : TRUE;
35 g rava rmensagemdee r rono log = TRUE : TRUE;
36 TRUE : FALSE ;
37 e s a c ;
38 nex t ( g r ava rmensagemdee r rono log ) := case
39 g rava rmensagemdee r rono log = TRUE : TRUE;
40 a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o = TRUE & i n i c i a l e i t u r a d e r e g i s t r o s =
TRUE : FALSE ;
41 a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o = TRUE : {FALSE , TRUE} ;
42 TRUE : FALSE ;
43 e s a c ;
44 nex t ( i n i c i a l e i t u r a d e r e g i s t r o s ) := case
45 i n i c i a l e i t u r a d e r e g i s t r o s = TRUE : TRUE;
46 a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o = TRUE & ( g rava rmensagemdee r rono log =
TRUE | n ex t ( g r ava rmensagemdee r rono log = TRUE) ) : FALSE ;
47 a b r i r o r e p o s i t o r i o d e d a d o s d e d e s t i n o = TRUE & grava rmensagemdee r rono log =
FALSE : TRUE;
48 TRUE : FALSE ;
49 e s a c ;
50 nex t ( l e p r o x im o r e g i s t r o ) := case
51 l e p r o x im o r e g i s t r o = TRUE : TRUE;
52 l e p r o x im o r e g i s t r o = FALSE & i n i c i a l e i t u r a d e r e g i s t r o s = TRUE |
e x c l u i o r e g i s t r o n o r e p o s i t o r i o = TRUE : TRUE;
53 TRUE : FALSE ;
54 e s a c ;
55 nex t ( e x c l u i t odo so smapeamen t o s ) := case
56 exc l u i t odo so smapeamen t o s = TRUE : TRUE;
57 l e p r o x im o r e g i s t r o = TRUE & t o d o s o s r e g i s t r o s j a f o r am e x c l u i d o s = TRUE :
FALSE ;
58 l e p r o x im o r e g i s t r o = TRUE : {FALSE , TRUE} ;
59 TRUE : FALSE ;
60 e s a c ;
95
61 nex t ( t o d o s o s r e g i s t r o s j a f o r am e x c l u i d o s ) := case
62 t o d o s o s r e g i s t r o s j a f o r am e x c l u i d o s = TRUE : TRUE;
63 l e p r o x im o r e g i s t r o = TRUE & ( exc l u i t odo so smapeamen t o s = TRUE | nex t (
e x c l u i t odo so smapeamen t o s = TRUE) ) : FALSE ;
64 l e p r o x im o r e g i s t r o = TRUE & exc l u i t odo so smapeamen t o s = FALSE : TRUE;
65 TRUE : FALSE ;
66 e s a c ;
67 nex t ( e x c l u i o r e g i s t r o n o r e p o s i t o r i o ) := case
68 e x c l u i o r e g i s t r o n o r e p o s i t o r i o = TRUE : TRUE;
69 e x c l u i o r e g i s t r o n o r e p o s i t o r i o = FALSE & exc l u i t odo so smapeamen t o s = TRUE :
TRUE;
70 TRUE : FALSE ;
71 e s a c ;
72 nex t ( g ravamensagemdesucesso ) := case
73 gravamensagemdesucesso = TRUE : TRUE;
74 gravamensagemdesucesso = FALSE & t o d o s o s r e g i s t r o s j a f o r am e x c l u i d o s = TRUE
: TRUE;
75 TRUE : FALSE ;
76 e s a c ;
77 nex t ( f e c h a r o r e p o s i t o r i o d e d a d o s ) := case
78 f e c h a r o r e p o s i t o r i o d e d a d o s = TRUE : TRUE;
79 f e c h a r o r e p o s i t o r i o d e d a d o s = FALSE & gravamensagemdesucesso = TRUE : TRUE;
80 TRUE : FALSE ;
81 e s a c ;
82 nex t ( f i n a l 0 2 ) := case
83 f i n a l 0 2 = TRUE : TRUE;
84 f e c h a r o r e p o s i t o r i o d e d a d o s = TRUE : TRUE;
85 TRUE : FALSE ;
86 e s a c ;
