Embed Size (px)
Citation preview
INSTITUTO MILITAR DE ENGENHARIA
CARLOS HENRIQUE DA COSTA OLIVEIRA
VERIFICAÇÃO DE MODELOS APLICADA AO PROJETODE SISTEMAS INDUSTRIAIS AUTOMATIZADOS POR
CONTROLADORES LÓGICOS PROGRAMÁVEIS
Dissertação de Mestrado apresentada ao Curso deMestrado em Engenharia Elétrica do Instituto Militarde Engenharia, como requisito parcial para obtenção dotítulo de Mestre em Ciências em Engenharia Elétrica.
Orientador: Antonio Eduardo Carrilho da Cunha - Dr.Eng.Co-orientador: Mario Cesar Mello Massa de Campos -Dr. ECP
Rio de Janeiro
2006
c2006
INSTITUTO MILITAR DE ENGENHARIAPraça General Tibúrcio, 80-Praia VermelhaRio de Janeiro-RJ CEP 22290-270
Este exemplar é de propriedade do Instituto Militar de Engenharia, que poderá incluí-loem base de dados, armazenar em computador, microfilmar ou adotar qualquer forma dearquivamento.
É permitida a menção, reprodução parcial ou integral e a transmissão entre bibliote-cas deste trabalho, sem modificação de seu texto, em qualquer meio que esteja ou venhaa ser fixado, para pesquisa acadêmica, comentários e citações, desde que sem finalidadecomercial e que seja feita a referência bibliográfica completa.
Os conceitos expressos neste trabalho são de responsabilidade do(s) autor(es) e do(s)orientador(es).
L48 Oliveira, Carlos Henrique da C.Verificação de Modelos Aplicada ao Projeto de Sistemas
Industriais Automatizados por Controladores Lógicos Pro-gramáveis / Carlos Henrique da Costa Oliveira. - Riode Janeiro : Instituto Militar de Engenharia, 2006.
108 p.: il, graf., tab.
Dissertação (mestrado) - Instituto Militar deEngenharia- Rio de Janeiro, 2006.
1. Controladores Lógicos Programáveis - CLP. 2. Sis-temas Industriais Automatizados. 3. Verificção de Mode-los. 4. Automação. 5. Confiabilidade. 6. Diagrama deBlocos Funcionais - DBF. I. Título. II. Instituto Militarde Engenharia.
CDD 629.895
2
INSTITUTO MILITAR DE ENGENHARIA
CARLOS HENRIQUE DA COSTA OLIVEIRA
VERIFICAÇÃO DE MODELOS APLICADA AO PROJETO DESISTEMAS INDUSTRIAIS AUTOMATIZADOS PORCONTROLADORES LÓGICOS PROGRAMÁVEIS
Dissertação de Mestrado apresentada ao Curso de Mestrado em Engenharia Elétricado Instituto Militar de Engenharia, como requisito parcial para obtenção do título deMestre em Ciências em Engenharia Elétrica.
Orientador: Antonio Eduardo Carrilho da Cunha - Dr. Eng.Co-orientador: Mario Cesar Mello Massa de Campos - Dr. ECP
Aprovada em 07 de Agosto de 2006 pela seguinte Banca Examinadora:
Antonio Eduardo Carrilho da Cunha - Dr. Eng. do IME - Presidente
Mario Cesar Mello Massa de Campos - Dr. ECP do CENPES
João Carlos dos Santos Basilio - Ph.D. da UFRJ
Paulo César Pellanda - Dr. ENSAE do IME
Rio de Janeiro2006
3
Aos meus pais, José Carlos de Oliveira Delgado eAdélia da Costa Oliveira, dedico esta conquista porserem o tesouro da minha vida.
4
AGRADECIMENTOS
A Deus.
Ao Instituto Militar de Engenharia, especialmente ao Departamentos de Engenharia
Elétrica, pela oportunidade de realizar este curso.
Aos meus pais José Carlos e Adélia, e irmãos Adriana, Claudio e Carlos Adriano, aos
meus cunhados Amauri e Esmeri e sobrinhas Lorraine, Catarine, Victoria e Lucas que
sempre me deram incentivo e motivação ao longo de toda a minha vida e em mais esta
etapa de minha formação.
Aos meus tio(a)s, vô, e primo(a)s por todo o incentivo e carinho.
A tia Sandra por todo o apoio.
A Denise, tia Vera, Sr Vitor, Fernanda e Marlon, que me acolheram com muito
carinho no Rio de Janeiro.
Aos meus amigos Cris, Faguinho, Rodrigo, Patrick, Charles, Marcinho, Raul, Pablo
e Diogo Couto pela alegria, incentivo e amizade.
Ao amigo, orientador e professor Antonio Eduardo Carrilho da Cunha pela paciência,
dedicação, incentivo e cumplicidade como orientador, sem os quais este trabalho não teria
se concretizado.
Ao amigo, co-orientador e professor Mario Cesar Mello Massa de Campos por acred-
itar e incentivar o trabalho.
Ao Marcelo do CENPES pelo apoio.
Aos professores Ades, Pellanda, Medling, Decilio e Pinheiro pelos conselhos, apoio e
profissionalismo prestados no decorrer do curso.
Aos meus amigos Leonardo Araújo, Diogo, Arthur, Michele, Alessandra, Rogério por
terem entrado na minha vida.
Aos amigos Wander, Pinho, Toscano Careca, Ten. Toscano, Ten. Gleison, Leozinho,
Luiz Felipe e Gilmar, pelo apoio, bizus e amizade.
Aos Professores Envandro Camelo, Hélio Paiva pelas cartas de recomendação para o
meu início no curso de mestrado.
Aos meus amigos Monique e Roberto pela força.
A todos que não foram citados mas contribuíram de alguma forma para o trabalho.
A Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES pelo apoio
financeiro.
5
SUMÁRIO
LISTA DE ILUSTRAÇÕES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
LISTA DE TABELAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
LISTA DE SÍMBOLOS E ABREVIATURAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1 INTRODUÇÃO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.1 Motivação e Justificativa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.2 Objetivos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.3 Metodologia . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.4 Organização do Trabalho . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2 VERIFICAÇÃO DE MODELOS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1 Visão Geral da Verificação de Modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1.1 A Necessidade de Métodos Formais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1.2 Verificação de Hardware e Software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.1.3 O Processo de Verificação de Modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.1.4 Lógica Temporal e Verificação de Modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.5 Algoritmos Simbólicos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2 Lógicas Temporais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2.1 A Lógica da Árvore da Computação CTL∗ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2.2 CTL e LTL. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.3 Exemplo - Exclusão Mútua . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.3 O Verificador de Modelos SMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.4 Resumo do Capítulo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3 VERIFICAÇÃO DE MODELOS APLICADA À PROGRAMAÇÃO
DE CLPS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.1 Controladores Lógicos Programáveis (CLPs) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.2 Visão Geral da Verificação de Modelos Aplicada à Programação de CLPs . . . 37
3.3 Um Modelo para os Diagramas de Contatos . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.4 Exemplos de Aplicação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.4.1 Sistema de Alarme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.4.2 Sistema de Manufatura . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
6
3.5 Resumo do Capítulo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
4 CONTRIBUIÇÕES À APLICAÇÃO DA VERIFICAÇÃO DE MO-
DELOS AO PROJETO DE SISTEMAS AUTOMATIZADOS . . . . . 57
4.1 Projeto de Sistemas Automatizados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
4.2 Exemplo de um Projeto de Sistema Automatizado . . . . . . . . . . . . . . . . . . . . . . . 59
4.2.1 Descrição Literal das Especificações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4.2.2 Matriz de Causa e Efeito . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4.2.3 Fluxograma de Funcionamento e Programa de Aplicação . . . . . . . . . . . . . . . . . 61
4.2.4 Programa em DBF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
4.3 Proposta de Verificação de Modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
4.4 Escrita da Especificação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.4.1 Escrita de Especificações a partir da Matriz de Causa e Efeito . . . . . . . . . . . . 63
4.4.2 Escrita das Especificações a partir do Conhecimento do Sistema . . . . . . . . . . . 67
4.5 A Tradução da linguagem DBF em código SMV . . . . . . . . . . . . . . . . . . . . . . . 67
4.5.1 Elementos de Lógica Booleana . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.5.2 Elementos de Memória . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.5.3 Blocos Temporizadores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
4.5.4 Construção Modular do Código . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
4.6 Verificação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.6.1 Reprojeto . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.7 Resumo do Capítulo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
5 APLICAÇÃO NA AUTOMAÇÃO DE UM AQUECEDOR A
CHAMA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
5.1 Automação do Processo de Purga . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
5.1.1 Seqüência de Purga . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
5.1.2 Lista de Entradas e Saídas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
5.1.3 Matriz de Causa e Efeito . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
5.1.4 Projeto do Programa em DBF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
5.2 Modelagem das Especificações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
5.3 Modelagem do Programa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
5.4 Verificação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
5.5 Resumo do Capítulo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
7
6 CONCLUSÃO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
6.1 Contribuições à verificação de modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
6.2 Limitações da Abordagem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
6.3 Perspectivas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
7 REFERÊNCIAS BIBLIOGRÁFICAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
8 APÊNDICE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
8.1 Manual do Verificador de Modelos Simbólicos (Symbolic Model Check-
ing - SMV) versão 2.5.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
8.2 Linguagem de Entrada . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
8.3 Sintaxe e Semântica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
8.3.1 Convenções Léxicas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
8.3.2 Expressões . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
8.3.3 Declaração da ASSIGN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
8.3.4 Declaração SPEC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
8.3.5 Declaração DEFINE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
8.3.6 Módulos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
8.3.7 Identificadores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
8.3.8 Módulo main . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
8
LISTA DE ILUSTRAÇÕES
FIG.2.1 (a) Estrutura Kripke. (b) Árvore correspondente para estado ini-
cial S0. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
FIG.2.2 Operadores básicos de CTL. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
FIG.2.3 Gráfico de transição de estados global para o problema de exclusão
mútua de um processo. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
FIG.3.1 Fluxo de dados entre o CLP e um sistema a controlar. . . . . . . . . . . . . . . . 36
FIG.3.2 Ciclo de varredura do CLP. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
FIG.3.3 Diagrama de Fluxo de Dados. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
FIG.3.4 LD e descrição do modelo equivalente. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
FIG.3.5 Sistema de alarme. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
FIG.3.6 Programa de Controle para o Sistema de Alarme. . . . . . . . . . . . . . . . . . . . 44
FIG.3.7 Representação do programa de controle do alarme em linguagem
de verificação de modelos. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
FIG.3.8 Verificação de Modelos para o programa de controle do alarme
(contra-exemplo). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
FIG.3.9 Contra-exemplo da especificação da linha 4 na Figura 3.8. . . . . . . . . . . . . 47
FIG.3.10 Analise gráfica do contra-exemplo da especificação da linha 4 na
Figura 3.8. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
FIG.3.11 Contra-exemplo da especificação da linha 7 na Figura 3.8. . . . . . . . . . . . . 49
FIG.3.12 Analise gráfica do contra-exemplo da especificação da linha 7 na
Figura 3.8. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
FIG.3.13 Reprojeto. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
FIG.3.14 Planta. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
FIG.3.15 Programa de Controle para o Sistema de Manufatura. . . . . . . . . . . . . . . . . 51
FIG.3.16 Representação do programa de controle da manufatura em lin-
guagem de verificação de modelos. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
FIG.3.17 Verificação de Modelos para o programa de controle da manufatura
(contra-exemplo). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
FIG.3.18 Analise gráfica do contra-exemplo da especificação na linha 7 da
Figura 3.16. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
FIG.3.19 Projeto com base na análise do contra-exemplo. . . . . . . . . . . . . . . . . . . . . . 56
FIG.3.20 Resposta da Verificação após correção do programa. . . . . . . . . . . . . . . . . . 56
9
FIG.4.1 Método de projeto adotado por Empresas de Automação. . . . . . . . . . . . . 58
FIG.4.2 Sistema estrela-triângulo. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
FIG.4.3 Matriz de Causa e Efeito do sistema Y −△. . . . . . . . . . . . . . . . . . . . . . . . . 60
FIG.4.4 Fluxograma para o sistema estrela-triângulo. . . . . . . . . . . . . . . . . . . . . . . . 61
FIG.4.5 Programa em Diagramas de Blocos Funcionais. . . . . . . . . . . . . . . . . . . . . . 62
FIG.4.6 Procedimento atual e proposta de modificação. . . . . . . . . . . . . . . . . . . . . . . 63
FIG.4.7 Escrita de especificações CTL. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
FIG.4.8 Blocos lógicos AND, OR e NOT. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
FIG.4.9 Blocos SET/RESET. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
FIG.4.10 Códigos SET/RESET. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
FIG.4.11 Blocos dos temporizadores DI, DT, PO. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
FIG.4.12 Máquinas de estado correspondente ao código do temporizador DI. . . . . . 70
FIG.4.13 Máquinas de estado correspondente ao código do temporizador DT. . . . . 71
FIG.4.14 Máquinas de estado correspondente ao código do temporizador PO. . . . . 71
FIG.4.15 Códigos dos temporizadores. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
FIG.4.16 Programa em Diagramas de Blocos Funcionais com as variáveis
auxiliares. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
FIG.4.17 Tradução do DBF em código SMV. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
FIG.4.18 Resposta da verificação. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
FIG.4.19 Contra-exemplo da especificação na linha 7 da Figura 4.18. . . . . . . . . . . . 76
FIG.4.20 Contra-exemplo da especificação na linha 10 da Figura 4.18. . . . . . . . . . . 77
FIG.4.21 Contra-exemplo da especificação na linha 13 da Figura 4.18. . . . . . . . . . . 78
FIG.4.22 Reprojeto com base no contra-exemplo. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
FIG.4.23 Reprojeto na linguagem SMV. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
FIG.5.1 Matriz de Causa e Efeito do sistema Purga. . . . . . . . . . . . . . . . . . . . . . . . . 83
FIG.5.2 Projeto do sistema Purga. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
FIG.5.3 Tipos de sinal, segundo a norma ISA 5.2 (ISA, 1992). . . . . . . . . . . . . . . . . 84
FIG.5.4 Projeto do sistema Purga com inserção de variáveis auxiliares. . . . . . . . . 88
FIG.5.5 Modelo do Programa no SMV. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
FIG.5.6 Resposta da verificação do sistema Purga. . . . . . . . . . . . . . . . . . . . . . . . . . . 90
FIG.8.1 Listagem de short.smv. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
FIG.8.2 Expressão . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
FIG.8.3 Programa e expressões reusáveis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
FIG.8.4 Atribuição . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
10
LISTA DE TABELAS
TAB.3.1 Simbologia e descrição dos diagramas de contato . . . . . . . . . . . . . . . . . . . . 40
TAB.3.2 Bobinas do sistema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
TAB.4.1 Entradas e saídas do sistema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
TAB.4.2 Condições para representação das Saídas . . . . . . . . . . . . . . . . . . . . . . . . . . 65
TAB.5.1 Variáveis de entrada do sistema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
TAB.5.2 Variáveis de saída do sistema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
11
LISTA DE SÍMBOLOS E ABREVIATURAS
ABREVIATURAS
CLP - Controlador Lógico Programável
IME - Instituto Militar de Engenharia
LD - Diagrama de Contatos
SMV - Verificador de Modelo Simbólico
CTL - Lógica da Árvore da Computação
LTL - Lógica Temporal Linear
SIPN - Rede de Petri Interpretada a Sinais
SFC - Diagrama de Função Sequencial
PN - Rede de Petri
SED - Sistema a Eventos Discretos
TCS - Teoria de Controle Supervisório
DBF - Diagrama de Blocos de Funções
BF - Blocos de Funções
IL - Lista de Instruções
ST - Texto Estruturado
SIS - Sistema Instrumentado de Segurança
MCE - Matriz de Causa e Efeito
P&I - Diagrama de Processo e Instrumentação
MIE - Memória Intermediária de Entrada
MIS - Memória Intermediária de Saída
OBDD - Diagrama de Decisão Binária Ordenado
DCS - Sistemas de Controle Distribuído
SÍMBOLOS
: - tal que
∃ - existe
∀ - para todo
12
⇒ - se, então
⇔ - se, somente se
∨ - operador OU
∧ - operador E
¬ - operador NÃO
a ∈ A - a pertence ao conjunto A
a /∈ A - a não pertence ao conjunto A
≡ - equivalente
s |= f - f é válido no estado s
s 2 f - f não é válido no estado s
A ⊂ B - A está contido em B
A ⊃ B - B está contido em A
A ≥ B - A maior ou igual a B
A ≤ B - A menor ou igual a B
A < B - A menor que B
A > B - A maior que B
SIMBOLOGIA PARA ALGORITMOS
! - operador NÃO
| - operador OU
& - operador E
:= - atribuição
init(x) - operador de inicialização da variável x
next(x) - operador de próximo estado da variável x
− > - operador implica
== - operador igual
! = - operador diferente
< - operador menor que
<= - operador menor ou igual que
> - operador maior que
>= - operador maior ou igual que
13
RESUMO
A confiabilidade é um fator fundamental para os Sistemas Industriais Automatizados.Assim, é importante que o programa de aplicação do Controlador Lógico Programável(CLP), responsável pelo processo, atenda às corretas especificações para o funcionamento.A não conformidade com as especificações, seja por implementação errônea de uma lógicaou pela não observação de aspectos da interação do CLP com os equipamentos externos,pode levar a prejuízos materiais, pessoais e ambientais. O objetivo deste trabalho éaplicar as técnicas de verificação de modelos (model checking) ao projeto de SistemasIndustriais Automatizados baseados em CLPs programados por Diagramas de BlocosFuncionais (DBFs). As contribuições deste trabalho são: Criação de um procedimentode tradução de programas escritos em DBF para a linguagem reconhecida pela ferramentade verificação SMV usando carimbos, descrever um padrão para escrever especificações nalinguagem da Lógica da Árvore da Computação CTL e propõe uma etapa de reprojeto,com base no contra exemplo.
14
ABSTRACT
Reliability is a basic factor for an industrial automated system. Thus, it is impor-tant that the application program running in the Programmable Logic controller (PLC),responsible for the system, follows exactly the safety specifications. The nonconformitywith the specifications, either by an error in the program implementation or by thenonobservation of some aspects of the interleaving logic, may lead to material, personalor environmental damages. The aim of this work is to apply model checking techniques tothe project of industrial automated system based on PLCs. Particularly the verificationis performed using the software SMV and the program in the PLC is implemented inFunctional Block Diagrams (FBDs). The contributions of this work are: a systematicprocedure for the translation of the structures in a FBD program into SMV code usingtemplates, and a method to re-project the PLC software by using of counterexamplesgiven in the verification procedures.
15
1 INTRODUÇÃO
Este capítulo apresenta uma visão geral do trabalho, incluindo uma introdução ao
problema tratado, os objetivos traçados, a metodologia adotada e um guia de leitura
desta dissertação.
1.1 MOTIVAÇÃO E JUSTIFICATIVA
A confiabilidade é um fator fundamental para os Sistemas Industriais Automatizados.
Assim, é importante que o programa de aplicação no Controlador Lógico Programável
(CLP) responsável pelo processo industrial atenda às corretas especificações para o seu
funcionamento. Uma implementação que fuja do comportamento esperado pode permi-
tir que ocorram falhas, possibilitando a ocorrência de acidentes e prejuízos de ordem
material, pessoal e ambiental. Veja-se, por exemplo, o problema na planta química em
ALIPERTI (2005) e o problema no projeto das esteiras do aeroporto de Denver em GIBBS
(1994). Este trabalho é baseado na necessidade real de se utilizarem métodos formais em
sistemas onde falhas são inaceitáveis.
A verificação de modelos surgiu na ciência da computação na década de 60 em torno
da crise crônica do software (GIBBS, 1994). Começou a ser empregada na Engenharia
de Automação mais recentemente com a crescente complexidade dos sistemas autom-
atizados. O processo de verificação de modelos consiste basicamente em modelagem,
especificação e verificação.
A Verificação de Modelos permite fazer a comparação entre as especificações do
Sistema Industrial Automatizado e o programa a ser implementado no CLP. No caso
de não conformidade do projeto com as especificações, a verificação fornece um contra-
exemplo que ilustra a divergência.
Procedimentos semelhantes foram descritos em MOON (1994), RAUSCH & KROGH
(1998) e SMET & ROSSI (2002). Entretanto tais trabalhos tratam apenas de programas
escritos em linguagem por diagramas de contato e não tratam da sistematização do uso
da verificação num procedimento de projeto de um Sistema Industrial Automatizado.
16
1.2 OBJETIVOS
O objetivo do presente trabalho é aplicar a Verificação de Modelos como técnica aux-
iliar para o projeto de Sistemas Industriais Automatizados por CLP. Deseja-se garantir
principalmente a confiabilidade do sistema implementado. Particularmente, neste tra-
balho, trata-se da programação de CLPs por Diagramas de Blocos Funcionais (DBFs).
Este trabalho visa criar um procedimento de tradução do programa de aplicação
em DBF para um código aceito pela ferramenta de verificação. Objetiva-se tornar o
programa modular, no qual é possível inserir modelos dos equipamentos externos, dos
blocos temporizadores e dos blocos de memórias sob a forma de carimbos.
Também tem como objetivo sistematizar o procedimento de tradução de especifi-
cações em propriedades formais a serem verificadas.
1.3 METODOLOGIA
Primeiramente foi feito um estudo dos principais métodos de validação para sistemas
complexos, como: simulação, teste, verificação dedutiva e verificação de modelos, que é
a adotada no trabalho.
Em seguida é feito um estudo de Controladores Lógicos Programáveis (CLPs) e suas
principais linguagens de programação dando uma visão geral do processo de verificação
de modelos com exemplos de MOON (1994) e RAUSCH & KROGH (1998).
Com base numa generalização das etapas do projeto de um Sistema Industrial Autom-
atizado por CLPs, propõem-se etapas adicionais onde se aplica a verificação de modelos
para validar o projeto. Para a execução da Verificação é utilizada a ferramenta SMV
(Symbolic Model Verifier), que é uma ferramenta acadêmica que representa o estado-
da-arte em verificação de modelos (CMU, 2000). Com base no contra exemplo, este
trabalho propõe uma etapa de reprojeto do programa de aplicação. Tais procedimentos
são descritos na Seção 4.3.
Conseqüentemente, o trabalho descreve uma metodologia sistematizada para a veri-
ficação de modelos em projetos de sistemas automatizados, criando um procedimento de
tradução de programas escritos em Diagramas de Blocos Funcionais (DBF) para a lin-
guagem reconhecida pela ferramenta de verificação SMV. Descreve também um padrão
para escrever especificações baseadas no conhecimento do sistema e na matriz de causa
e efeito na linguagem da Lógica da Árvore da Computação CTL. Após desenvolvida a
metodologia, aplica-se a um exemplo real de parte de um Aquecedor a Chama no Capítulo
17
5.
1.4 ORGANIZAÇÃO DO TRABALHO
O Capítulo 2 dá uma visão geral da verificação de modelos, descrevendo o seu pro-
cesso. Mostra o sistema de verificação de modelos que MCMILLAN (1993) desenvolveu
como parte de sua tese de doutorado, que é utilizado neste trabalho. Também apresenta
o que é a lógica da árvore de computação (CTL).
O Capítulo 3 tem por principal objetivo mostrar como funciona a verificação de
programas de CLP usando a verificação de modelos. São utilizados exemplos acadêmicos
de sistemas de pequeno porte (RAUSCH & KROGH, 1998) e (MOON, 1994) para facilitar
o entendimento do processo de verificação.
O Capítulo 4 tem por objetivo aplicar as técnicas de verificação de modelos ao projeto
de Sistemas Automatizados baseados em CLPs programados por DBF. Foram desenvolvi-
dos padrões para a verificação, com base em estruturas lógicas típicas, como carimbos de
blocos de memória e temporizadores. Também foram desenvolvidos padrões de especi-
ficações para sistemas automatizados, visando a uma futura automatização do processo
de verificação.
O Capítulo 5 tem por objetivo aplicar as técnicas de verificação de modelos desen-
volvidas a uma parte de um projeto de automação de um Aquecedor a Chama Industrial.
O Capítulo 6 conclui o trabalho, analisando seu conteúdo em termos dos objetivos
propostos. Também neste capítulo são resumidas as contribuições teóricas realizadas e
apresentam-se ainda sugestões para futuros trabalhos.
18
2 VERIFICAÇÃO DE MODELOS
Este capítulo apresenta o método de verificação de modelos desenvolvido por Clarke
e Emerson (CLARKE et al., 1999), que é utilizado neste trabalho.
2.1 VISÃO GERAL DA VERIFICAÇÃO DE MODELOS
A Verificação de Modelos é uma técnica automática para validação do projeto de
sistemas concorrentes de estados finitos. Foi usada com sucesso na prática para vali-
dar projetos de complexos circuitos seqüenciais e protocolos de comunicação (CLARKE
et al., 1999). O principal desafio da verificação de modelos é o tratamento do problema
de explosão de espaço de estados. Este problema ocorre nos sistemas com muitos com-
ponentes que interagem entre si e com sistemas que possuem estruturas de dados que
podem assumir muitos valores diferentes. Nesta seção, compara-se a verificação de mo-
delos a outros métodos formais para validação de projetos de software e hardware. Além
disso, descreve-se como a verificação de modelos é usada para validar projetos de sistemas
complexos.
2.1.1 A NECESSIDADE DE MÉTODOS FORMAIS
Hoje, sistemas de hardware e software são usados amplamente em aplicações onde
falhas são inaceitáveis: comércio eletrônico, redes de comunicações telefônicas, estradas
de rodagem, sistemas de controle de tráfego aéreo, instrumentos médicos, entre outras.
Freqüentemente, escutam-se notícias de incidentes onde alguma falha é causada por um
erro em um sistema de hardware ou software. Um exemplo recente de tais falhas é o
foguete Ariane 5, que explodiu em 4 de junho de 1996, mais ou menos quarenta segundos
depois que foi lançado (SPARACO, 1996). O comitê que investigou o acidente mostrou
que este foi causado por um erro no software de um computador que era responsável por
calcular o movimento do foguete. Durante o lançamento, uma exceção ocorreu quando
um número de ponto flutuante de 64-bits foi convertido num inteiro de 16-bits com sinal.
Tal conversão não era protegida pelo código para manipular exceções e fez com que o
computador falhasse. O mesmo erro também fez com que o computador de backup fal-
hasse. Em conseqüência, dados incorretos da atitude foram transmitidos ao computador
de bordo, que causou a destruição do foguete. A equipe que investigou a falha sugeriu que
19
diversas medidas fossem tomadas a fim impedir incidentes similares no futuro, incluindo
a verificação do software do Ariane 5 (SPARACO, 1996).
Por causa do sucesso da Internet e dos sistemas embarcados nos automóveis, aero-
planos, e outros sistemas criticamente seguros, a dependência do correto funcionamento
de dispositivos computacionais se torna cada vez maior. De fato, o ritmo da mudança
se torna mais acelerado a cada ano. Por causa deste rápido crescimento na tecnologia, é
importante desenvolver métodos que aumentem a confiança na correção de tais sistemas.
2.1.2 VERIFICAÇÃO DE HARDWARE E SOFTWARE
Os principais métodos de validação para sistemas complexos são simulação, teste,
verificação dedutiva, e verificação de modelos (CLARKE et al., 1999). Ambos, simulação
e teste, envolvem a execução de experimentos antes de se empregar o sistema. Enquanto
se executa a simulação sobre uma abstração ou modelo do sistema, o teste é executado
no produto real. No caso de circuitos, a simulação é executada no projeto do circuito,
enquanto o teste é executado no próprio circuito. Em ambos os casos, estes métodos
injetam sinais em determinados pontos no sistema e observam os sinais resultantes em
outros pontos. Para o software, a simulação e os testes geralmente envolvem a geração de
determinadas entradas e observação das saídas correspondentes. Estes métodos podem
ser uma maneira econômica para encontrar diversos erros. Entretanto, verificar todas as
interações possíveis e falhas potenciais usando simplesmente as técnicas de simulação e
teste é raramente possível.
O termo verificação dedutiva se refere normalmente ao uso de axiomas e regras de
prova para demonstrar a corretude dos sistemas (CLARKE et al., 1999). No início da
pesquisa envolvendo verificação dedutiva, o foco principal estava em garantir a correção
de sistemas críticos. Supunha-se que a importância do comportamento correto era tão
grande que o projetista ou perito em verificação (geralmente um matemático ou um
logicista) deveria gastar o tempo que fosse necessário para verificar o sistema. Inicial-
mente, tais provas eram construídas inteiramente à mão. Com o tempo, os pesquisadores
descobriram que ferramentas de software poderiam ser desenvolvidas para forçar o uso
correto de axiomas e regras de prova. Tais ferramentas poderiam também aplicar uma
busca sistemática para sugerir várias maneiras de se progredir no estágio corrente da
prova.
A importância da verificação dedutiva é amplamente reconhecida pelos cientistas
da computação. A técnica influenciou significativamente a área de desenvolvimento de
20
softwares (por exemplo, a noção de um invariante). Entretanto, a verificação dedutiva é
um processo demorado que pode ser efetuado somente por peritos treinados no raciocínio
lógico e que tenham considerável experiência. A prova de um simples protocolo ou circuito
pode durar dias ou meses (CLARKE et al., 1999). Conseqüentemente, o uso da verificação
dedutiva é raro. É aplicado primordialmente aos sistemas altamente sensíveis, tais como
protocolos de segurança, onde o investimento de recursos necessários para garantir a
segurança do seu uso são justificáveis.
É importante estar ciente de que algumas tarefas matemáticas não podem ser ex-
ecutadas por algoritmos. A teoria da computabilidade (CLARKE et al., 1999) fornece
limitações do que pode ser decidido por um algoritmo. Em particular, mostra-se que
não existe um algoritmo que decida se um programa de computador arbitrário (escrito
em alguma linguagem de programação como C ou Pascal) termina. Isto limita imediata-
mente o que pode ser verificado automaticamente. Mais ainda, a terminação correta de
um programa genérico não pode ser verificada automaticamente (CLARKE et al., 1999).
Dessa forma, uma grande parte dos sistemas de prova não podem ser completamente
automatizados.
Uma vantagem da verificação dedutiva é que esta pode ser usada para especular sobre
sistemas de estados infinitos (CLARKE et al., 1999). E esta tarefa pode ser automati-
zada dentro de certos limites. E ainda, mesmo que a propriedade a ser verificada seja
verdadeira, nenhum limite pode ser colocado na quantidade de tempo ou de memória
necessária a se encontrar uma solução.
A verificação de modelos (model checking) é uma técnica para verificar sistemas con-
correntes de estados finitos (CLARKE et al., 1999). Um benefício desta restrição é que
a verificação pode ser executada automaticamente. O procedimento utiliza normalmente
uma busca exaustiva do espaço de estados do sistema para determinar se alguma especi-
ficação é verdadeira ou não. Dados os recursos suficientes, os procedimentos terminarão
sempre com uma resposta do tipo sim ou não. Além disso, pode ser implementada por
algoritmos com eficiência considerável, que podem rodar em máquinas potentes (geral-
mente não em um computador desktop típico).
Embora a restrição aos sistemas de estados finitos possa parecer uma principal
desvantagem, a verificação de modelos é aplicável a diversas classes importantes de sis-
temas. Os controladores de hardware são sistemas de estados finitos, e os mesmos são
muitos protocolos de comunicação. Em alguns casos, os sistemas que não são de esta-
dos finitos podem ser verificados pelo uso da verificação de modelos em combinação com
21
vários princípios de abstração e indução. Em muitos casos, erros podem ser encontra-
dos restringindo as estruturas de dados ilimitadas a instâncias específicas que sejam de
estados finitos. Por exemplo, programas com filas de mensagens ilimitados podem ser
tratados por restrição do tamanho das filas a um número pequeno como dois ou três.
Em virtude da verificação de modelos poder ser feita automaticamente, esta é prefer-
ível à verificação dedutiva sempre que puder ser aplicada. Entretanto, sempre haverá
algumas aplicações críticas em que a prova de teoremas é necessária para a verificação
completa. Um novo sentido da pesquisa tenta integrar a verificação dedutiva com a verifi-
cação de modelos, de modo que porções de estados finitos de sistemas complexos possam
ser verificadas automaticamente. (CLARKE et al., 1999)
2.1.3 O PROCESSO DE VERIFICAÇÃO DE MODELOS
Aplicar a verificação de modelos a um projeto consiste de basicamente três tarefas
(CLARKE et al., 1999):
• Modelagem: A primeira tarefa é converter um projeto em um formalismo aceito
por uma ferramenta de verificação de modelos. Em muitos casos, esta é simples-
mente uma tarefa de compilação. Em outros casos, devido a limitações em tempo
e memória, modelar um projeto requer o uso de abstração para eliminar detalhes
irrelevantes ou sem importância.
• Especificação: Antes da verificação, é necessário indicar as propriedades a que o
projeto deve satisfazer. A especificação é dada geralmente em algum formalismo
lógico. Para sistemas de hardware e de software, é comum usar a lógica temporal,
que pode afirmar como o comportamento do sistema evolui com o tempo. Um ponto
importante na especificação é a abrangência (completeness). Embora a verificação
de modelos forneça subsídios para se certificar de que um modelo satisfaz a uma
dada especificação, é impossível determinar se a especificação dada cobre todas as
propriedades a que o sistema deve satisfazer.
• Verificação: A verificação é completamente automática. Entretanto, na prática,
envolve, freqüentemente, o auxílio humano. Uma atividade manual é a análise dos
resultados da verificação. Caso dê um resultado negativo, é fornecido ao usuário
um traço de erro. O traço de erro trata de um contra-exemplo para a propriedade
verificada e se destina a auxiliar o projetista a detectar onde o erro ocorreu. Neste
22
caso, a análise do traço de erro pode requerer uma modificação no sistema e uma
nova aplicação do algoritmo de verificação.
Um traço de erro pode também resultar de uma modelagem incorreta do sistema
ou de uma especificação incorreta, chamada freqüentemente de negativo falso (CLARKE
et al., 1999). O traço de erro pode também ser útil para identificar e reparar estes dois
problemas. Uma outra possibilidade é que a tarefa da verificação não termine normal-
mente, devido ao tamanho do modelo, nos casos em que este seja demasiadamente grande
para a memória do computador. Neste caso, pode ser necessário refazer a verificação após
modificar alguns dos parâmetros do verificador de modelos ou ter-se ajustado o modelo
(por exemplo, pelo uso de abstrações adicionais).
2.1.4 LÓGICA TEMPORAL E VERIFICAÇÃO DE MODELOS
As lógicas temporais são úteis para especificar os sistemas concorrentes, porque de-
screvem a ordenação temporal dos eventos sem introduzir explicitamente o tempo. Foram
desenvolvidas originalmente por filósofos para investigar a maneira como o tempo é us-
ado nos argumentos da linguagem natural (HUGUES & CRESWELL, 1977). Embora
uma quantidade de lógicas temporais diferentes tenham sido desenvolvidas, a maioria
possui um operador como Gf que é verdadeiro no presente se f for sempre verdadeiro
no futuro (isto é, se f for globalmente verdadeiro). Para afirmar que dois eventos e1
e e2 nunca ocorrem ao mesmo tempo, escreve-se G(¬e1 ∨ ¬e2). As lógicas temporais
são classificadas freqüentemente conforme o tempo, sendo suposto ter em uma estrutura
linear ou ramificada. Neste trabalho, o sentido de uma fórmula em lógica temporal é
determinado sempre com respeito a um tipo de grafo de transição de estados, chamado,
por razões históricas, de estrutura Kripke (HUGUES & CRESWELL, 1977), conforme
mostra a Seção 2.2.1.
A introdução de algoritmos de verificação de modelos usando lógica temporal por
Clarke e Emerson (CLARKE & EMERSON, 1981) no início dos anos 80 permitiu a
automação do raciocínio em lógica temporal para validação de programas. O algoritmo
desenvolvido por Clarke e Emerson para a lógica de tempo ramificado CTL é polinomial
no tamanho do modelo determinado pelo programa sob consideração e no comprimento
de sua especificação em lógica temporal. Mostraram também como a imparcialidade
(fairness) poderia ser tratada sem alterar a complexidade do algoritmo.
Aproximadamente ao mesmo tempo, Quielle e Sifakis (QUIELLE & SIFAKIS, 1982)
produziram um algoritmo de verificação de modelos para um subconjunto da CTL, mas
23
a complexidade não foi analisada. Mais tarde Clarke, Emerson e Sistla (CLARKE et al.,
1986) planejaram um algoritmo melhorado linear no produto do comprimento da fór-
mula e do tamanho do grafo de transição de estados. O algoritmo foi implementado no
verificador de modelos denominado EMC, que foi distribuído e usado amplamente para
verificar diversos sistemas de protocolos de rede e circuitos seqüenciais (CLARKE et al.,
1999).
2.1.5 ALGORITMOS SIMBÓLICOS
Na implementação original do algoritmo de verificação de modelos de Clarke e Emer-
son (CLARKE & EMERSON, 1981), as relações de transição são representadas explici-
tamente por listas de adjacência. Para sistemas concorrentes com um pequeno número
de processos, o número dos estados é geralmente pequeno, e a abordagem é, em geral
viável. Nos sistemas com muitas partes concorrentes entretanto, o número de estados no
grafo de transição de estados global é muito grande para lidar. Em 1987, Ken McMil-
lan, então um estudante de pós-graduação na Universidade de Carnegie Mellon, descobriu
que, usando uma representação simbólica para os grafos de transição de estados, sistemas
com número de estados muito maior poderiam ser verificados (MCMILLAN, 1993). A
nova representação simbólica foi baseada nos Diagramas de Decisão Binária Ordenados
(Ordered Binary Decision Diagrams - OBDDs), (BRYANT & MUSGRAVE, 1998). Os
OBDDs fornecem uma forma canônica que é freqüentemente mais compacta que a forma
normal conjuntiva ou disjuntiva (CLARKE et al., 1999). Algoritmos eficientes foram
desenvolvidos para manipular fórmulas booleanas escritas em OBDDs. Uma vez que a
representação simbólica captura alguma regularidade no espaço de estados de determi-
nados circuitos e protocolos, é possível verificar sistemas com um número extremamente
grande de estados, muitas ordens maior do que poderia ser tratado pelos algoritmos que
explicitam espaços de estados. Usando o algoritmo de verificação de modelos original de
CTL de Clarke e Emerson com a nova representação para grafos de transição de estados,
tornou-se possível verificar alguns exemplos com mais de 1020 estados (CLARKE et al.,
1999). Desde então, os vários refinamentos das técnicas baseadas em OBDD por outros
pesquisadores levaram à contagem de estados de até mais de 10120 (CLARKE et al.,
1999).
A representação implícita é completamente natural para modelar circuitos seqüenciais
e protocolos. Cada estado é codificado por uma atribuição de valores booleanos ao
conjunto de variáveis de estado associadas ao circuito ou protocolo. A relação de transição
24
pode conseqüentemente ser expressa como uma fórmula booleana nos termos de dois
conjuntos de variáveis: um conjunto que codifica o estado de origem e o outro que codifica
o de destino. Esta fórmula é, então, representada por um diagrama binário de decisão
(CLARKE et al., 1999). O algoritmo de verificação de modelos se baseia no cálculo de
pontos fixos dos transformadores de predicado que são obtidos da relação de transição
(CLARKE et al., 1999). Os pontos fixos são conjuntos de estados que representam as
várias propriedades temporais do sistema concorrente. Nas novas implementações, tanto
os transformadores de predicado como os pontos fixos são representados por OBDDs.
Assim, é possível evitar que se construa explicitamente o grafo de estados do sistema
concorrente.
O sistema de verificação de modelos que McMillan desenvolveu como parte de sua
tese de doutorado é chamado Verificador de Modelos Simbólicos (Symbolic Model Veri-
fier - SMV) (MCMILLAN, 1993). Baseia-se em uma linguagem para descrever sistemas
concorrentes de estados finitos hierárquicos. Os programas na linguagem do SMV podem
ser verificados por especificações expressas em lógica temporal. O verificador de modelos
extrai um sistema de transição representado por um OBDD a partir de um programa na
linguagem SMV e usa um algoritmo de busca baseado em OBDDs para determinar se o
sistema satisfaz à especificação. Se o sistema de transição não satisfaz a alguma especi-
ficação, o verificador produzirá um traço de execução que mostra porque a especificação
é falsa. O sistema SMV é amplamente distribuído, e um grande número de exemplos
tem sido verificados com o mesmo. Os exemplos tratados fornecem uma evidência con-
vincente de que o SMV pode ser usado para eliminar erros em projetos industriais reais
(CLARKE et al., 1999). Uma descrição completa da linguagem SMV é apresentada no
Apêndice 8.1 deste trabalho.
Um exemplo que ilustra o poder da verificação simbólica de modelos é a verificação
do protocolo de coerência de cache descrito no padrão IEEE Futurebus+ (Padrão IEEE
896.1-1991) (CLARKE et al., 1999). O desenvolvimento do protocolo de coerência de
cache Futurebus+ data de 1988, e todas as tentativas precedentes de validar o protocolo
foram baseadas inteiramente em técnicas informais. No verão de 1992, pesquisadores da
Universidade Carnegie Mellon construíram um modelo preciso do protocolo na linguagem
SMV e, então, usaram o SMV para mostrar que o sistema de transição resultante satisfazia
uma especificação formal da coerência cache (CLARKE et al., 1993) e (LONG, 1993).
Foram capazes de encontrar uma certa quantidade de erros anteriormente não detectados,
bem como erros potenciais no projeto do protocolo. Clarke, Grumberg e Peled referem-
25
se a esta como sendo a primeira vez que uma ferramenta automática de verificação é
utilizada para encontrar erros num padrão IEEE (CLARKE et al., 1999).
2.2 LÓGICAS TEMPORAIS
Nesta seção é descrita uma lógica para especificar propriedades temporais dos sis-
temas de transição de estados. A lógica utiliza proposições atômicas e conectivos
booleanos tais como a conjunção, a disjunção, e a negação para construir elaboradas
expressões que descrevem as propriedades dos estados do sistema. A lógica temporal
é um formalismo para descrever seqüências de transições entre estados em um sistema
reativo. Na lógica temporal considerada, o tempo não é mencionado explicitamente, pelo
contrário, uma fórmula especifica se algum estado é eventualmente alcançado, ou que
um estado de erro nunca é atingido. As propriedades como eventualmente ou nunca são
especificadas usando-se operadores temporais (CLARKE et al., 1999).
2.2.1 A LÓGICA DA ÁRVORE DA COMPUTAÇÃO CTL∗
Conceitualmente, as fórmulas da lógica da árvore de computação (Computation Tree
Logic - CTL∗) descrevem propriedades de árvores da computação. Forma-se uma árvore
de computação ao se designar um estado de uma estrutura de transição de estados como
estado inicial e, então, desenrola-se a estrutura numa árvore infinita com o estado inicial
na raiz.
A semântica CTL∗ é definida com respeito a uma estrutura Kripke (CLARKE et al.,
1999). Sejam AP um conjunto de proposições atômicas, M é uma estrutura Kripke tripla
(S, R, L), onde S é o conjunto de estados; R ⊂ S × S é a relação de transição, que deve
ser total (isto é, para todos os estados s ∈ S existe um estado s ’ ∈ S tal que (s, s ’) ∈
R); e L : S → 2AP é uma função que etiqueta cada estado (s ∈ S ) com um conjunto
de proposições atômicas (L(s) ⊂ AP) verdadeiras nesse estado. Um caminho em M é
uma infinita seqüência de estados, π = s0, s1, ... tais que, para cada i ≥ 0, (si, si+1) ∈ R. A
Figura 2.1 (a) ilustra uma estrutura Kripke e a Figura 2.1 (b) mostra a sua correspondente
árvore da computação, com estado inicial s0 (CLARKE et al., 1986). Da Figura 2.1, o
conjunto de estados é S = {s0, s1, s2}, a relação de transição é R = {(s0, s1), (s1,s0),
(s0, s2), (s2, s1)}, e os conjuntos de proposições atômicas são AP = {a, b, c}, o conjunto
de proposições verdadeiras nos estados é P (s0) = {a, b}, P (s1) = {b, c} e P (s2) = {a, c}.
26
DE
DF
EF
S0
S2
S1
S0
S1 S2
S1
S0
S0
S1 S2
(a) (b)
.
.
....
.
.
.
FIG. 2.1: (a) Estrutura Kripke. (b) Árvore correspondente para estado inicial S0.
Em CTL∗ as fórmulas são compostas de quantificadores de caminho e operadores
temporais. Os quantificadores de caminho são usados para descrever a estrutura de
ramificação da árvore de computação. Há dois quantificadores de caminho: A (para
todos os caminhos de computação - for all computation paths) e E (para algum caminho
de computação - for some computation path). Estes quantificadores são usados em um
estado particular para especificar que todos ou algum dos caminhos que começam neste
estado possuem alguma propriedade. Os operadores temporais descrevem propriedades
de um caminho ao longo da árvore. Há cinco operadores temporais básicos:
• X (próxima vez - next time) requer que uma propriedade seja válida no segundo
estado do caminho.
• F (eventualmente ou no futuro - eventually or in the future) afirma que uma pro-
priedade é válida em algum estado do caminho.
• G (sempre ou globalmente - always or globally) especifica que uma propriedade é
válida para todo estado do caminho.
• U (até - until) é um operador que combina duas propriedades. Dadas as pro-
priedades p1 e p2, p1 U p2 se houver um estado do caminho onde p2 torna-se válida,
e em cada estado precedente, p1 sempre for válida.
• R (liberação - release) é dual ao operador U. Dadas as propriedades p1 e p2, p1
R p2, é válida quando p2 é válido ao longo do caminho até e incluindo o primeiro
27
estado onde p1 seja válido. Não se requer que p1 torne-se válido no caminho.
Há dois tipos de fórmulas em CTL∗: fórmulas de estado (que são verdadeiras em um
estado específico) e fórmulas de caminho (que são verdadeiras ao longo de um caminho
específico). Seja AP o conjunto de nomes de proposição atômicas. A sintaxe de fórmulas
de estado é dada pelas seguintes regras:
• Se p ∈ AP, então p é uma fórmula de estado.
• Se f e g são fórmulas de estado, então ¬f, f ∨ g e f ∧ g são fórmulas de estado.
• Se f é uma fórmula de caminho, então E f e A f são fórmulas de estado.
Duas regras adicionais são necessárias para especificar a sintaxe de fórmulas do cam-
inho:
• Se f é uma fórmula de estado, então f é também uma fórmula de caminho.
• Se f e g são fórmulas de caminho, então ¬f, f ∨ g e f ∧ g, X f, F f, G f, f U g, e
f R g são fórmulas de caminho.
A CTL∗ é o conjunto das fórmulas de estado geradas pelas regras acima.
Utiliza-se πi para denotar o sufixo do caminho π que começa no estado si. Se f
denotar uma fórmula de estado, a notação M,s |= f significa que f é válida no estado s
da estrutura kripke M. Similarmente, se f for uma fórmula de caminho, M,π |= f significa
que f é válida ao longo do caminho π na estrutura kripke M. Quando a estrutura kripke
M estiver subentendida no contexto, será usualmente omitida. A relação |= é definida
indutivamente como segue (supõe-se que f1 e f2 sejam as fórmulas de estado, g1 e g2 sejam
fórmulas de caminho e que π denote um caminho na forma S0 S1 S2...):
a) M, s |= f1 ⇔ f1 ∈ L(s).
b) M, s |= ¬f1 ⇔ M, s 2 f1.
c) M, s |= f1 ∨ f2 ⇔ M, s |= f1 ou M, s |= f2.
d) M, s |= f1 ∧ f2 ⇔ M, s |= f1 e M, s |= f2.
e) M, s |= Eg1 ⇔ há um caminho π a partir de s tal que M, π |= g1.
f) M, s |= Ag1 ⇔ para cada caminho π que parte de s, M, π |= g1.
28
g) M, π |= f1 ⇔ s é o primeiro estado de π e M, s |= f1.
h) M, π |= ¬g1 ⇔ M, π 2 g1.
i) M, π |= g1 ∨ g2 ⇔ M, π |= g1 ou M, π |= g2.
j) M, π |= g1 ∧ g2 ⇔ M, π |= g1 e M, π |= g2.
k) M, π |= Xg1 ⇔ M, π1 |= g1.
l) M, π |= Fg1 ⇔ existe um k ≥ 0 tal que M,πk |= g1.
m) M, π |= Gg1 ⇔ para todo i ≥ 0,M, πi |= g1.
n) M, π |= g1Ug2 ⇔ existe um k ≥ 0, tal que M, πk |= g2 e para todo 0 ≤ j <
k,M, πj |= g1.
o) M, π |= g1Rg2 ⇔ para todo j ≥ 0, se para cada i < j M, πi2 g1 então M,πj |= g2.
É fácil ver que os operadores ∨,¬,X,U, e E são suficientes para expressar qualquer
fórmula CTL∗ CLARKE et al. (1999), pois é possível listar o seguinte:
• f ∧ g ≡ ¬(¬f ∨ ¬g)
• fRg ≡ ¬(¬fU¬g)
• Ff ≡ verdadeiroUf
• Gf ≡ ¬F¬f
• A(f) ≡ ¬E(¬f)
2.2.2 CTL E LTL
Neta seção consideram-se duas sub-lógicas da CTL∗: uma é uma lógica de tempo
ramificante e a outra é uma lógica de tempo linear. A distinção entre as duas está na forma
como lidam com a ramificação na árvore de computação subjacente. Na lógica temporal
de tempo ramificante, os operadores temporais quantificam sobre os caminhos que são
possíveis a partir de um dado estado. Na lógica temporal de tempo linear, os operadores
são fornecidos descrevendo eventos ao longo de um único trajeto de computação.
A lógica da árvore da computação (CTL) é um subconjunto restrito da CTL∗ onde
cada um dos operadores temporais X, F, G, U e R deve ser imediatamente precedido
29
por um quantificador de caminho (CLARKE et al., 1999). Mais precisamente, a CTL é
um subconjunto da CTL∗ que é obtida ao se restringir a sintaxe de fórmulas de caminho
pela seguinte regra:
• Se f e g forem fórmulas de estado, então X f, F f, G f, f U g, e f R g são fórmulas
de caminho.
A Lógica temporal linear (LTL), consiste das fórmulas que têm a forma A f, onde
f é uma fórmula do caminho em que as únicas subfórmulas de estado permitidas são
proposições atômicas (CLARKE et al., 1999). Mais precisamente, uma fórmula de cam-
inho LTL é tal que:
• Se p ∈ AP, então p é uma fórmula de caminho.
• Se f e g são fórmulas de caminho, então ¬f, f∨ g, f∧ g, X f, F f, G f, f U g, e f R
g são fórmulas de caminho.
Pode-se mostrar que as três lógicas discutidas neste trabalho possuem poderes de
expressão diferentes (CLARKE et al., 1999). Por exemplo, não há nenhuma fórmula
CTL que seja equivalente à fórmula LTL A(FGp). Esta fórmula expressa a propriedade
de que, ao longo de todo caminho, há algum estado a partir do qual p será sempre
válido. Do mesmo modo, não há nenhuma fórmula LTL que seja equivalente à uma
fórmula CTL AG(EFp). A disjunção entre as duas fórmulas A(FGp) ∨ AG(EFp) é
uma fórmula CTL∗ e não é exprimível em fórmulas CTL ou LTL.
Todas as especificações neste trabalho serão escritas na lógica CTL. Há dez oper-
adores básicos de CTL (CLARKE et al., 1999):
• AX e EX;
• AF e EF;
• AG e EG;
• AU e EU;
• AR e ER.
Cada um dos dez operadores podem ser expressos nos termos de três operadores EX,
EG e EU (CLARKE et al., 1999):
30
• AXf = ¬EX(¬f)
• EFf = E[V erdadeiroUf ]
• AGf = ¬EF(¬f)
• AFf = ¬EG(¬f)
• A[fUg] ≡ ¬E[¬gU(¬f ∧ ¬g)] ∧ ¬EG¬g
• A[fRg] ≡ ¬E[¬fU¬g]
• E[fRg] ≡ ¬A[¬fU¬g]
Alguns dos principais operadores são ilustrados na Figura 2.2. Os operadores são mais
fáceis de compreender em termos da árvore da computação obtida pelo desdobramento
do modelo Kripke. Cada árvore da computação possui o nó s0 como raiz (CLARKE
et al., 1999).
Muitos dos métodos para evitar o problema da explosão de estados baseiam-se no
raciocínio computacional ou na abstração. A lógica que é usada tipicamente nestes casos
é mais restrita e apenas permite quantificadores de caminho universais. A limitação da
CTL aos quantificadores de caminho universais é chamada de ACTL∗, e a restrição da
CTL aos quantificadores de caminho universais é chamada ACTL.
A fim de evitar quantificadores de caminho existenciais implícitos resultantes do uso
da negação, supõe-se que as fórmulas sejam dadas na forma normal positiva, isto é, as
negações são aplicadas apenas às proposições atômicas. Para evitar perda do poder de
expressão, tornam-se necessários os operadores de junção (∧) e disjunção (∨), bem como
ambos os operadores U e de R.
31
f
f f
f
f
f f
f
f f
M,s0 _�$)�f M,s0_�$*�f
f
f
f
f
M,s0 _�()�f M,s0 _�(*�f
f f
M,s0 _�$;�f
f
M,s0 _EX f
s0 s0 s0
s0s0s0
FIG. 2.2: Operadores básicos de CTL.
As fórmulas AF AGa e AF AXa são exemplos de fórmulas ACTL. Essas fórmulas
não são exprimíveis em LTL CLARKE et al. (1999). Porque ACTL é um subconjunto de
CTL, as lógicas ACTL e LTL são incomparáveis. Além disso, ACTL∗ possui mais poder
de expressão que a LTL. As fórmulas AG EF a e AG¬ AF a não estão em ACTL.
2.2.3 EXEMPLO - EXCLUSÃO MÚTUA
Os grafos de transição de estados globais de muitos programas concorrentes podem
ser modelados como estruturas Kripke CLARKE et al. (1986). Por exemplo, a Figura
2.3 mostra a estrutura Kripke para uma solução simples do problema de exclusão mútua
entre dois processos P1 e P2. Nesta solução, cada processo Pi(i = 1ou2) está sempre em
uma de três regiões do código:
• Ni: fora da região crítica;
• Ti: esperando para entrar na região crítica;
• Ci: dentro da região crítica.
32
FIG. 2.3: Gráfico de transição de estados global para o problema de exclusão mútua deum processo.
Note que somente transições entre regiões diferentes do código foram modeladas;
os movimentos dentro da mesma região são considerados irrelevantes neste nível de ab-
stração. Além disso, cada transição é devido à execução exata de uma etapa de um
processo. É fácil ver, neste caso, que AF(C1) é verdadeiro no estado 1 e que EF(C1∧C2)
é falso no estado 0.
2.3 O VERIFICADOR DE MODELOS SMV
O SMV é uma ferramenta para verificar se sistemas de estados finitos satisfazem a
especificações dadas em CTL. Utiliza o algoritmo simbólico de verificação de modelos
baseado em OBDDs de McMillan (MCMILLAN, 1993) (CLARKE et al., 1999). Os
componentes da linguagem do SMV são usados para descrever sistemas complexos de
estados finitos. Algumas das características mais importantes da linguagem são descritas
abaixo.
O usuário pode decompor a descrição de um sistema de estados finitos complexo
em módulos. Os módulos podem ser instanciados diversas vezes, e podem referenciar
variáveis declaradas em outros módulos. Os módulos podem ter parâmetros que podem
ser componentes de estados, expressões, ou outros módulos.
Os Módulos do SMV podem ser compostos sincronamente ou por intertravamento.
Em uma composição síncrona, um passo na composição corresponde a um passo em cada
um dos componentes. No intertravamento, um passo da composição representa um passo
dado por apenas um componente. Se a palavra chave process preceder uma instância
de um módulo, o intertravamento é usado, senão a composição síncrona é suposta.
33
As transições de estado em um modelo podem ser deterministas ou não-
deterministas. O não-determinismo pode refletir um ponto de escolha nas ações do
sistema que está sendo modelado, ou pode ser usado para descrever um modelo mais
abstrato onde são omitidos determinados detalhes. A habilidade de especificar o não-
determinismo está ausente para muitas linguagens de descrição de hardware, mas é crucial
ao fazer modelos de alto nível (CLARKE et al., 1999).
As relações de transição dos módulos podem ser especificadas explicitamente nos
termos de relações booleanas nos estados estimados atuais e próximos de variáveis de
estados, ou implicitamente como um conjunto de indicações de atribuições paralelas. As
indicações de atribuição paralelas definem os valores das variáveis no próximo estado em
termos de valores no estado atual.
Não é fornecida uma sintaxe ou uma semântica formal para a linguagem do SMV
aqui neste capítulo, mas pode ser encontrado no manual do SMV (MCMILLAN, 1993)
ou no Apêndice 8.1.
2.4 RESUMO DO CAPÍTULO
Este capítulo mostra basicamente como funciona o método de Verificação de Modelos.
No próximo capítulo será mostrado como a verificação de modelos é aplicada à validação
de programas de CLP.
34
3 VERIFICAÇÃO DE MODELOS APLICADA À PROGRAMAÇÃO DE
CLPS
Este capítulo ilustra a aplicação da verificação de modelos à validação de progra-
mas de CLP. Os programas em consideração são escritos na linguagem de diagramas de
contato. Os exemplos apresentados servem de base para a compreensão de como são
elaboradas as especificações em CTL, e como funciona o método de verificação.
3.1 CONTROLADORES LÓGICOS PROGRAMÁVEIS (CLPS)
Um controlador lógico programável (CLP) é um equipamento eletrônico de tecnolo-
gia digital que utiliza memória programável para armazenamento interno de instruções
para cumprimento de rotinas especificas, como lógica, seqüenciamento, temporização,
contagem e aritmética, para controlar, por intermédio dos sinais provenientes de módu-
los de entradas e saídas, vários tipos de máquinas ou processos (DIAS, 2005). A Figura
3.1 apresenta um fluxo de dados de um CLP e um processo sob seu controle (MOON,
1994). Ao controlar um sistema, um CLP executa repetidamente um ciclo de varredura
conforme mostra a Figura 3.2. Um ciclo de varredura tipo consiste em três etapas:
a) Atualização dos dados da memória intermediária de entrada (MIE) com base nos
valores lidos nos módulos de entrada.
b) Execução sequencial do programa de aplicação do usuário, com alteração da
memória de dados.
c) Escrita dos valores da memória intermediária de saída (MIS) nos módulos de saída.
35
FIG. 3.1: Fluxo de dados entre o CLP e um sistema a controlar.
Para que o CLP seja um controlador eficaz, o tempo de varredura deve ser menor
do que o tempo de duração mais curto de um sinal de entrada ou saída do processo. O
tempo de varredura é geralmente na escala de milesegundos e depende da velocidade do
processador, do tamanho do programa, e do número de dispositivos de entrada e de saída
(FALCIONE & KROGH, 1993).
FIG. 3.2: Ciclo de varredura do CLP.
O padrão IEC 61131-3 (IEC, 2003) define a sintaxe e a semântica de cinco linguagens
de programação para CLPs. As quatro primeiras linguagens de programação são: os Dia-
gramas de Contatos, os Diagramas de Blocos Funcionais (que são linguagens gráficas), os
Textos Estruturados e as Listas de Instruções (que são linguagens textuais). A linguagem
de Diagramas de Contato (Ladder Diagram - LD) se baseia na lógica de relés e permite
a descrição de funções Booleanas. Na linguagem dos Diagramas de Blocos Funcionais
36
(DBF), a programação é feita por intermédio de blocos gráficos. A linguagem de Texto
Estruturado (Structured Text - ST), próxima ao Pascal, permite sentenças condicionais,
seqüenciais e laços. A Lista de Instruções (Instruction List - IL) é uma linguagem na
forma de um código assembler.
A quinta linguagem da norma IEC 61131-3 é definida para estruturar a organização
interna dos programas de CLP e blocos de funções. Esta linguagem gráfica, chamada
de Cartas de Funções Seqüenciais (Sequential Function Charts - SFC), trata de uma
extensão das máquinas de estado contendo primitivas para descrever comportamentos
seqüenciais, paralelismo e sincronicidades. Permite a divisão de um programa de CLP
(ou bloco de funções) em um conjunto de etapas e transições interconectadas por arcos
direcionados. Cada etapa é associada a um conjunto de ações e cada transição é associada
a um conjunto de condições lógicas. Baseia-se no Grafcet, norma IEC 60848 (IEC, 1999).
Um dos objetivos da IEC 61131-3 é proporcionar ao projetista de programas de CLP
uma ferramenta modular e estruturante para viabilizar a reusabilidade e a qualidade
dos programas, especialmente em direção à confiabilidade à segurança (LAMPÉRIÈRE-
COUFFIN et al., 1999). Todavia, a existência de elementos comuns para todas as lin-
guagens de programação não é o bastante para assegurar a qualidade dos programas, e
o padrão não trata de métodos eficientes de verificação.
3.2 VISÃO GERAL DA VERIFICAÇÃO DE MODELOS APLICADA À PROGRA-
MAÇÃO DE CLPS
Encontram-se na literatura algumas abordagens para verificação de programas de
CLP, descritas sucintamente a seguir. Em MOON (1994), apresenta-se um método de
verificação de programas escritos em diagrama de contatos. Definem-se algumas formas
de escrever as especificações em CTL para os acionamentos típicos de um CLP. Mostra-se
uma forma de modelagem de um programa escrito em diagrama de contatos na forma de
um código SMV. Utiliza a ferramenta SMV original (CMU, 2000) para fazer a verificação.
Em RAUSCH & KROGH (1998), utiliza-se o formalismo dos sistemas Condição/Evento
para representar a planta a controlar pelo CLP. Dessa forma, inclui-se o modelo dos
equipamentos externos que interfaceiam com o CLP. Utilizam-se módulos para descrever
os componentes do sistema e do programa do CLP. Em VÖLKER & KRÄMER (1999)
faz a verificação por prova de teoremas assistida por uma ferramenta de software. As
especificações são escritas em LTL e os programas a verificar descritos em SFCs e DBFs.
Em SMET & ROSSI (2002) modela-se uma célula de manufatura onde se testam 90
37
especificações. Utiliza-se o Cadence SMV (CADENCE, 2002) para fazer a verificação.
Expressam-se as propriedades em LTL e CTL. Em XIYING & LITZ (2002) utilizam-se
redes de Petri para modelar o sistema. Apresenta-se um procedimento para descrever os
sistemas por Redes de Petri Interpretadas a Sinais (SIPN). SONG et al. (2004) faz a ver-
ificação de modelos para programas com blocos temporizadores. Trata-se da verificação
de propriedades para a automação de usinas nucleares.
A Figura 3.3 apresenta uma visão geral do método a ser seguido para se executar
a verificação de sistemas automatizados por CLP baseado nas abordagens de MOON
(1994) e RAUSCH & KROGH (1998), citadas anteriormente.
Programas em Diagrama de Contatos
Equipamentos/sensores/atuadores/processo
Modelo do prog. em Diagr. deCont. em execução no CLP
Contra-exemplo
Propriedades formais
Funcionamento do CLP
Especificações de funcionamento
Modelo do sistema
Verificação
Propriedade verdadeira
Modelo do ambienteexterno
FIG. 3.3: Diagrama de Fluxo de Dados.
Primeiramente obtém-se um modelo do programa de aplicação combinado ao fun-
cionamento do CLP. De forma geral, tratam-se apenas programas escritos em Diagramas
de Contatos. As estruturas utilizadas da linguagem de diagrama de contatos são simples,
não se encontrando na maioria das abordagens, estruturas complexas do tipo memórias,
temporizadores etc. Essa modelagem do programa de aplicação, incluindo sua interpre-
tação pelo hardware do CLP, foi estabelecida por MOON (1994). A verificação é feita
sobre uma abstração do programa e não sobre o programa de aplicação propriamente
dito. Faz-se uma modelagem da listagem do CLP na linguagem do SMV apenas.
Adicionalmente, pode-se ter o modelo do ambiente externo ao CLP: equipamentos,
sensores, atuadores e o processo propriamente dito. Isso enriquece o modelo do sistema,
restringindo os comportamentos possíveis, pois nem todo sinal de entrada pode ocorrer. A
38
modelagem do ambiente externo ao CLP foi estabelecida pela primeira vez por RAUSCH
& KROGH (1998).
O modelo do programa de aplicação, combinado ao modelo do funcionamento do
CLP, e o modelo do ambiente externo são combinados num modelo do sistema a verificar,
como mostrado na Figura 3.3.
As especificações de funcionamento podem descrever as seqüências lógicas indese-
jadas, a lógica de sequencialização ou as propriedades estruturais do sistema. Em função
da descrição das especificações ou do conhecimento do sistema, é feita a construção da
propriedade formal, escrita na maioria das vezes em CTL. Não se observa na literatura
nenhuma tentativa de sistematização da escrita de especificações.
Em geral a verificação é feita utilizando-se diferentes versões da ferramenta SMV.
MOON (1994) e RAUSCH & KROGH (1998) desenvolveram os estudos sobre SMV
original (CMU, 2000). SMET & ROSSI (2002) utilizam o Cadence SMV (CADENCE,
2002). Há, ainda, a ferramenta NuSMV (CAVADA & CIMATTI, 2004).
O resultado da verificação indica se o modelo do sistema está em conformidade com
as especificações ou não. Em caso negativo, três são as hipóteses que devem ser levan-
tadas, como indicado pelo tracejado na Figura 3.3. Primeiramente, uma fonte de não
conformidade é o erro de modelagem do sistema. Neste caso, deve-se refinar ou corrigir o
modelo do sistema para se fazer uma nova verificação. A segunda hipótese é a existência
de um erro do programa de aplicação captado na modelagem. Neste caso, deve-se par-
tir para um reprojeto do programa antes de uma nova verificação. A terceira hipótese
corresponde ao dito falso verdadeiro de uma propriedade, onde as especificações ou estão
escritas incorretamente ou expressam requisitos muito restritos para o sistema. Neste
caso, a especificação deve ser reescrita para uma nova verificação.
3.3 UM MODELO PARA OS DIAGRAMAS DE CONTATOS
Os Diagramas de Contato são uma forma de programação de CLPs por meio de
símbolos gráficos, representando contatos e bobinas. Os contatos e bobinas correspondem
a variáveis booleanas armazenadas na memória de dados do CLP. São conectados por
ligações em ramos (rungs) como num diagrama de lógica a relé. As expressões booleanas
calculadas a cada ciclo de varredura do CLP correspondem à avaliação lógica seqüencial
do diagrama de contatos (FABIAN & HELLGREN, 1998).
Um contato é representado como abaixo, onde se identifica um contato, associado à
variável booleana A, interna ao CLP, e duas ligações: uma à direita e uma à esquerda.
39
A
--| |--
Os contatos são usados como acesso ao estado de uma variável interna no cálculo de
expressões booleanas. Tipicamente encontram-se os contatos indicados na Tabela 3.1
(FABIAN & HELLGREN, 1998).
TAB. 3.1: Simbologia e descrição dos diagramas de contato
CONTATO SÍMBOLO DESCRIÇÃOContato normal-mente aberto
A
--| |--
O estado da ligação à esquerda é copiado para a ligaçãoà direita se o estado de A é verdadeiro, caso contrário,o estado da ligação à direita é falso.
Contato normal-mente fechado
A
--|/|--
O estado da ligação à esquerda é copiado para a ligaçãoà direita se o estado de A é falso, caso contrário, o estadoda ligação à direita é falso.
Uma bobina é representada como abaixo, onde identifica-se uma bobina associada a
uma variável booleana Q, interna ao controlador, e duas ligações: uma à direita e uma à
esquerda.
Q
--( )--
As bobinas alteram os estados de suas variáveis associadas. A Tabela 3.2 ilustra alguns
tipos de bobina (FABIAN & HELLGREN, 1998).
TAB. 3.2: Bobinas do sistema
BOBINA SÍMBOLO DESCRIÇÃOBobina normal Q
--( )--
O estado da ligação da esquerda é copiado para avariável Q.
Bobina negativa Q
--(\)--
A negação do estado da ligação à esquerda é copi-ada para a variável Q.
A conversão de um diagrama de contatos para uma descrição de modelo em SMV é
quase que uma correspondência direta (MOON, 1994). Os valores de saída das bobinas,
à direita de cada ramo, dependem da estrutura e dos valores no lado esquerdo do ramo.
Cada ramo pode ser convertido em uma descrição de modelo correspondente usando os
operadores do SMV ! (NÃO), & (E), | (OU) e next (próximo estado) (MOON, 1994).
40
A Figura 3.4 mostra um diagrama de contatos (a) e a descrição do modelo equivalente
no SMV (b). As barras verticais do diagrama indicam a fonte de potência, onde a barra
da esquerda representa o potencial alto e a barra da direita representa o potencial baixo,
enquanto as linhas horizontais, chamadas ramos, indicam, os fluxos corrente possíveis. A
varredura dos ramos de um diagrama de contatos é da esquerda superior para a direita.
Dependendo do fabricante do CLP, a varredura do diagrama de contatos é feita ramo a
ramo ou coluna a coluna. Em muitos casos, as duas ordens não fazem nenhuma diferença
no comportamento da varredura dos CLPs. Para evitar casos excepcionais, é escolhido
o modelo do diagrama de contatos fazendo varredura ramo a ramo de cima para baixo
(MOON, 1994). A ordem da varredura coluna por coluna pode ser modelada de uma
maneira similar (MOON, 1994).
next(R2) := R1;
next(R4) := !R3;
next(R7) := R5 & R6;
next(R10) := R8 | R9;
next(R15) := next(R7) & R14;
next(R12) := (R11 | R12) & !R13;
Ramo 1
Ramo 2
Ramo 3
Ramo 4
Ramo 5
Ramo 6
R1 R2
R3 R4
R6 R7
R11
R12
R13
R7 R14 R15
R8
R9
R10
R5
R12
(a) (b)
FIG. 3.4: LD e descrição do modelo equivalente.
O ramo 1 do diagrama da Figura 3.4, corresponde a um contato normalmente aberto
R1 ligado a uma bobina de saída R2. O valor correspondente da bobina R2 no próximo
ciclo de varredura é igual ao valor do contato R1 no tempo de varredura atual. Deste
modo, se a entrada R1 é VERDADEIRA então R2 é VERDADEIRA no próximo ciclo
de varredura; senão R2 é FALSO no próximo ciclo de varredura.
41
Embora a memória de dados seja atualizada imediatamente enquanto as entradas
relacionadas são mudadas, o sinal de saída ocorre depois, uma vez feita a varredura.
Para incluir a idéia da diferença de tempo entre a entrada e a saída, o operador next
é usado na descrição de modelos como mostrado no texto do lado direito (b) da Figura
3.4. O ramo 2 representa a lógica booleana (NÃO) e a descrição de modelos equivalentes
é mostrada no texto usando o operador !.
Os ramos em série e paralelo de variáveis de entrada representam a lógica booleana
E e OU, respectivamente, como mostrado nos ramos 3 e 4. Por exemplo, R7 no ramo
3 é VERDADEIRO na próxima varredura somente se R5 e R6 são atualmente VER-
DADEIROS. O ramo 5 mostra um contato de selo, uma estrutura fundamental para
todos os elementos armazenados. A bobina R12 torna-se VERDADEIRA (selagem) se
o contato de R11 tornar VERDADEIRO, e R12 permanece VERDADEIRA até que o
contato R13 se torne VERDADEIRO (liberação). A descrição de modelo equivalente é
mostrada no texto da Figura 3.4. Observe que R12 é mostrado como um contato nor-
malmente aberto no lado direito do texto e uma saída representada pelo operador next
no lado esquerdo do texto. Porque R7 no ramo 6 é mostrado também no ramo 3 como
uma saída, o contato R7 já está alterado quando o CLP começa a varredura do ramo 6
(somente na ordem de varredura ramo a ramo de cima para baixo). Assim o valor de R7
no ramo 6 é o mesmo que o próximo valor R7 mudado no ramo 3. O R7 no ramo 6 é
representado como next(R7) em vez de R7, mesmo R7 sendo mostrado no lado esquerdo
do ramo. A regra da conversão aqui é que se a variável da entrada já tiver aparecido
como uma variável de saída acima do ramo atual, o operador next deve ser adicionado
para representar a variável na descrição de modelos do SMV.
Pode-se traduzir um programa em Diagrama de Contatos em um modelo do sistema
correspondente para sua verificação usando as regras da conversão mostradas na Figura
3.4.
3.4 EXEMPLOS DE APLICAÇÃO
Nesta seção são apresentados dois exemplos acadêmicos que ilustram como é feita a
verificação em diagramas de contato. Tratam-se de um sistema de alarme fornecido por
MOON (1994) e um sistema de manufatura fornecido por RAUSCH & KROGH (1998).
42
3.4.1 SISTEMA DE ALARME
Considere um típico sistema de alarme mostrado na Figura 3.5 (MOON, 1994). O
sistema possui duas entradas binárias: um sinal vindo de um contato no campo (d1), a
significar a ocorrência de uma condição, e o sinal de reconhecimento da condição, por
parte do operador (APB) vindo de uma botoeira num painel. Duas saídas binárias: uma
sirene (horn) e uma lâmpada de advertência (lig). Cada variável binária assume o valor 1
(VERDADEIRO) ou 0 (FALSO). O estado d1 = 1 indica que alguma condição no campo
excede um limite permitido, por exemplo, um reator está em uma alta temperatura ou é
detectada a pressão baixa num processo.
Sistema de Alarme Lâmpada (lig)Reconhecimento (APB)
Condição no campo (d1) Sirene (horn)
FIG. 3.5: Sistema de alarme.
As especificações informais do projeto para o diagrama de contatos deste sistema de
alarme são as seguintes:
• Se a condição no campo ocorre (d1 = 1 ), o sistema de alarme faz soar a sirene
(horn = 1 ).
• Nessa condição, quando o operador pressiona a botoeira de reconhecimento (APB
= 1 ), o sistema deve desligar a sirene e acender a lâmpada de advertência (lig =
1 ).
• A lâmpada permanece acesa enquanto persistir a condição no campo (d1 = 1 ).
• Assim que a condição no campo cessar (d1 = 0 ), a lâmpada deve ser apagada (lig
= 0 ) e o sistema retorna à condição inicial de normalidade.
Suponha que um engenheiro projete o diagrama de contatos para o sistema de alarme
mostrado na Figura 3.6 baseado nas especificações acima (MOON, 1994).
Utiliza-se o método de verificação para certificar-se de que o programa atende a todas
as especificações dadas. Como a primeira etapa da verificação, é necessário modelar o
programa de controle.
A Figura 3.7 mostra o programa de controle na linguagem de descrição de modelos
da ferramenta SMV (MOON, 1994). As linhas 12 a 14 da Figura 3.7 iniciadas por next
43
d1horn
R1 d1horn
horn
APB
d1 APB
lig d1
lig
d1 R1
R1
APB
horn APB
R1
FIG. 3.6: Programa de Controle para o Sistema de Alarme.
correspondem a cada ramo mostrado na Figura 3.6. Toda vez que ocorre a varredura no
CLP, as variáveis dependentes, R1, horn e lig, mudam de acordo com as regras de cada
ramo. As linhas 9 e 11 correspondem à inicialização das variáveis internas ao CLP.
1 MODULE main
2 VAR
3 d1: boolean;
4 APB : boolean;
5 R1 : boolean;
6 horn : boolean;
7 lig : boolean;
8 ASSIGN
9 init(R1) := 0;
10 init(horn) := 0;
11 init(lig) := 0;
12 next(R1) := ((!d1 & (APB |!horn)) | R1) & ((!horn & !APB) | !d1);
13 next(horn) := ((next(R1) & d1) | horn) & !APB;
14 next(lig) := ((d1 & APB) | lig) & (next(R1) | d1);
15
16 SPEC AG(APB -> AF !horn)
17 SPEC AG(!d1 & !APB -> AX(d1 & !APB -> AF horn))
18 SPEC AG(horn -> !E[!APB U (!horn & !APB)])
19 SPEC AG(!d1 -> AF !lig)
20 SPEC AG(d1 & !APB -> AX(d1 & APB -> AF lig))
21 SPEC AG(lig -> !E[d1 U (!lig & d1)])
22 SPEC AG!(horn & lig)
FIG. 3.7: Representação do programa de controle do alarme em linguagem deverificação de modelos.
44
As linhas 16 a 22 da Figura 3.7 mostram as especificações escritas em CTL referentes
à descrição do sistema. As três primeiras (linhas 16 a 18) expressam o comportamento
da sirene, as três seguintes (linha 19 a 21) comportamento da lâmpada e a última (linha
22) comportamento conjunto da sirene e da lâmpada.
O resultado da verificação é mostrado de forma parcial, na Figura 3.8.
1 -- specification AG (APB -> AF (!horn)) is true
2 -- specification AG (!d1 & !APB -> AX (d1 & !APB -> AF ho... is true
3 -- specification AG (horn -> !E((!APB) U (!horn & !APB))) is true
4 -- specification AG (!d1 -> AF (!lig)) is false
5 -- specification AG (d1 & !APB -> AX (d1 & APB -> AF lig)... is true
6 -- specification AG (lig -> !E(d1 U (!lig & d1))) is true
7 -- specification AG (!(horn & lig)) is false
FIG. 3.8: Verificação de Modelos para o programa de controle do alarme(contra-exemplo).
A primeira especificação
AG(APB− > AF!horn)
faz o verificador de modelos procurar todas as possibilidades de estados no sistema e
responder à pergunta: se a botoeira for acionada, faz a sirene parar? A resposta do
verificador de modelos a esta pergunta é VERDADEIRA como mostrado na linha 1 da
Figura 3.8.
A segunda especificação
AG(!d1&!APB− > AX(d1&!APB− > AFhorn))
corresponde a se a botoeira não estiver pressionada e, no próximo instante, o sinal de
perigo em d1 muda de 0 para 1, então a sirene soa. O verificador de modelos responde
que este teste é VERDADEIRO como mostrado na linha 2 da Figura 3.8.
A terceira especificação
AG(horn− >!E[!APBU(!horn&!APB)])
testa o período de tempo em que a sirene soa. A segunda parte da expressão CTL é
!E[!APBU(!horn&!APB)],
equivalente a A[hornUAPB], que significa que a sirene permanece VERDADEIRA a
menos que APB seja VERDADEIRA. A especificação mostra um caso, em que uma vez
45
a sirene acionada, permanece ligada a menos que a botoeira seja pressionada. A botoeira
não pode ser pressionada para sempre. A resposta é VERDADEIRA como mostrado
na linha 3 da Figura 3.8. Os resultados dos três testes acima indicam que a sirene se
comporta como especificado no enunciado do problema.
As três especificações seguintes tratam do comportamento da lâmpada de advertên-
cia. A expressão CTL
AG(!d1− > AF!lig)
significa que a lâmpada não acende sem que a condição no campo ocorra. Como visto na
Figura 3.8 (linha 4) a resposta é FALSA. Isto significa que há um estado em que a lâmpada
permanece ligada (lig=1 ) quando não há nenhuma condição no campo (d1=0 ). Deve-se
seguir o contra-exemplo fornecido pelo SMV e mostrado na Figura 3.9 para encontrar
a fonte do erro, o que é ilustrado na Figura 3.10. A condição inicial mostra que todas
as variáveis são zero (VERDADE). A condição no campo (d1 ), a botoeira (APB) e R1
são mostradas VERDADEIRAS no estado 1.2. A lâmpada torna-se VERDADEIRA no
estado 1.3 e permanece ligada mesmo que a condição no campo desapareça. Um exemplo
é o loop dos estados 1.3 ao 1.5. Este contra-exemplo pode sugerir uma modificação no
projeto, particularmente na parte da lógica relacionada à lâmpada. As duas especificações
seguintes para a lâmpada (linhas 5 e 6 da Figura 3.8) são análogas às especificações
correspondentes da sirene.
46
1 -- specification AG (!d1 -> AF (!lig)) is false
2 -- as demonstrated by the following execution sequence
3 state 1.1:
4 d1 = 0
5 APB = 0
6 R1 = 0
7 horn = 0
8 lig = 0
9
10 state 1.2:
11 d1 = 1
12 APB = 1
13 R1 = 1
14
15 -- loop starts here --
16 state 1.3:
17 d1 = 0
18 APB = 0
19 R1 = 0
20 lig = 1
21
22 state 1.4:
23 d1 = 1
24 APB = 1
25 R1 = 1
26
27 state 1.5:
28 d1 = 0
29 APB = 0
30 R1 = 0
FIG. 3.9: Contra-exemplo da especificação da linha 4 na Figura 3.8.
47
d1
APB
R1
horn
lig
1.1 1.2 1.3 1.4 1.5Estados
Local onde ocorre o problema
FIG. 3.10: Analise gráfica do contra-exemplo da especificação da linha 4 na Figura 3.8.
A especificação
AG!(horn&lig)
testa se há alguma situação que a sirene e a lâmpada estão ligadas simultaneamente. A
resposta é FALSA visto que no estado 1.5 da Figura 3.11 a sirene (horn) e a lâmpada
(lig) estão em simultaneidade, conforme ilustra a analise gráfica na Figura 3.12.
48
1 -- specification AG (!(horn & lig)) is false
2 -- as demonstrated by the following execution sequence
3 state 1.1:
4 d1 = 0
5 APB = 0
6 R1 = 0
7 horn = 0
8 lig = 0
9
10 state 1.2:
11 d1 = 1
12 APB = 1
13 R1 = 1
14
15 state 1.3:
16 d1 = 0
17 APB = 0
18 R1 = 0
19 lig = 1
20
21 state 1.4:
22 d1 = 1
23 R1 = 1
24
25 state 1.5:
26 d1 = 0
27 horn = 1
FIG. 3.11: Contra-exemplo da especificação da linha 7 na Figura 3.8.
d1
APB
R1
horn
lig
1.1 1.2 1.3 1.4 1.5Estados
Local onde ocorre o problema
FIG. 3.12: Analise gráfica do contra-exemplo da especificação da linha 7 na Figura 3.8.
Para que a lâmpada funcione corretamente nesta situação, o diagrama de contatos
49
deve ser reprojetado. A Figura 3.10 ilustra uma possível solução por remoção de um
contato associado a R1 no terceiro ramo do diagrama de contatos. As mesmas especifi-
cações são usadas para verificar o diagrama de contatos reprojetado, e o resultado correto
para todos os testes relativos às especificações mostradas na Figura 3.8, após reprojeto
(Figura 3.13), asseguram ao usuário que o sistema de alarme segue as especificações
dadas. Observa-se que este método não garante qualquer coisa sobre comportamentos
não modelados do sistema.
d1horn
R1 d1horn
horn
APB
d1 APB
lig
lig
d1 R1
d1
APB
horn APB
R1
FIG. 3.13: Reprojeto.
3.4.2 SISTEMA DE MANUFATURA
Trata-se de um exemplo fornecido por RAUSCH & KROGH (1998), que consiste de
dois relés e de um pistão para mover uma peça (Figura 3.14). É parte de um sistema de
manufatura onde uma esteira transportadora move uma peça para a posição 1. O pistão
move a peça da posição 1 para a posição 2. Um outro pistão (não mostrado) move a peça
da posição 2 para outra esteira transportadora.
A Figura 3.14 mostra os sinais de saída binários do controlador c1 e c2, os quais são
sinais de entrada à planta, e os sinais de entrada binários do controlador R1on, R2on (=
1 se o relé for acionado), Pbase e Pestendido (= 1 se o pistão estiver nesta posição). O
pistão é movido por um motor controlado por dois relés. O relé R1 causa o movimento
para a diante, e o relé R2, o movimento inverso. A especificação para o sistema da Figura
50
3.14 é que se proíbe que ambos os relés estejam acionados simultaneamente.
M
Posição 2
Posição1
C1 C2
R1 R2
Pestendido
Pbase
R1on
R2on
Pistão
CLP
Peça
FIG. 3.14: Planta.
O controle é realizado usando um CLP, e é usada no exemplo a notação de diagramas
de contato. A Figura 3.15 mostra o programa no CLP (RAUSCH & KROGH, 1998),
onde R1on , R2on são os sinais do sensor dos relés, C1s, C2s são os sinais de comando
do controlador, e C1 e C2 são os sinais de saída de comando aos relés. A lógica de
controle deixa um comando a um relé para o controlador durante a passagem seqüencial
completa, desde que o outro relé não esteja acionado, ou não haja nenhum comando que
esteja se opondo à força para acionar o outro relé.
FIG. 3.15: Programa de Controle para o Sistema de Manufatura.
Em RAUSCH & KROGH (1998), por meio da verificação formal, prova-se que a ex-
51
ecução da lógica de controle está incorreta pois em algum momento do ciclo de varredura
ambos os relés podem ser acionados ao mesmo tempo.
Neste exemplo utilizam-se módulos para elaborar um modelo SMV para o sistema
(RAUSCH & KROGH, 1998). Um módulo é um gabarito para um sistema de transições
de estados que é usado para modelar múltiplos componentes em um sistema com múltiplas
instâncias. As instâncias dos módulos podem ser usadas nas definições de outros módulos,
dando a possibilidade para definir modelos hierárquicos de sistemas complexos (CLARKE
et al., 1999). Por exemplo, as linhas de 7 a 16 da Figura 3.16 mostram um módulo que
representa um relé genérico para o sistema.
Um módulo é definido pela palavra-chave MODULE e um nome seguido por uma lista de
variáveis de entrada (linha 1 da Figura 3.16). As variáveis locais do módulo são definidas
em uma lista que começa com a palavra chave VAR (linha 2). As transições de estados
são caracterizadas pelas mudanças nos valores das variáveis do módulo e definidas na
indicação de ASSIGN (linhas 10 a 16). As transições podem ser não-deterministas como
ilustrado nas linhas 13 e 14. Variáveis adicionais podem ser definidas depois da palavra
chave DEFINE, não mostrada neste programa.
As instâncias dos módulos podem ser usadas para construir outros módulos. No caso
em análise, um módulo que representa o sistema completo é composto por duas instâncias
dos módulos para os dois relés (que usam a mesma definição do módulo) e um módulo
para o controlador (vide Figura 3.16). Um programa pode ser instanciado mais de uma
vez como nas linhas 3 e 4. O módulo completo é referenciado pelo módulo principal main.
Este é o módulo superior na composição hierárquica como mostra as linhas de 1 a 6 da
Figura 3.16.
O diferencial deste exemplo é a necessidade de se modelar o ambiente externo ao
CLP, pois a especificação de comportamento consiste em evitar que os relés R1 e R2
estejam acionados ao mesmo tempo. O modelo se dá a partir da escrita de diagramas de
estados correspondentes ao comportamento desejado para os relés, como mostrado nas
linhas 7 a 16 da Figura 3.16.
O exemplo ilustra os tipos de circunstâncias sutis que podem conduzir a problemas
com programas de CLP, devido à duração finita do ciclo de varredura. A probabilidade da
seqüência de transições indesejadas ocorrer pode ser pequena, mas é certamente possível
(veja Figura 3.17).
Para melhor visualização do traço do contra-exemplo é apresentada uma análise
gráfica na Figura 3.18. Na computação da saída C2, há um teste para certificar se a
52
1 MODULE main
2 VAR
3 r1 : relay(c.C1);
4 r2 : relay(c.C2);
5 c : controller(r1.state,r2.state);
6 SPEC AG (!r1.state | !r2.state)
7 MODULE relay(input)
8 VAR
9 state : boolean;
10 ASSIGN
11 init(state) := 0;
12 next(state) := case
13 !state & input : {1,0};
14 state & !input : {0,1};
15 1: state;
16 esac;
17 MODULE controller(R1on,R2on)
18 VAR
19 C1s : boolean;
20 C2s : boolean;
21 C1 : boolean;
22 C2 : boolean;
23 ASSIGN
24 init(C1s) := 0;
25 init(C2s) := 0;
26 init(C1) := 0;
27 init(C2) := 0;
28 next(C1) := (C1s & (R1on | (!R2on & !C2)));
29 next(C2) := (C2s & (R2on | (!R1on & !next(C1))));
FIG. 3.16: Representação do programa de controle da manufatura em linguagem deverificação de modelos.
53
1 -- specification AG (!r1.state | !r2.state) is false
2 -- as demonstrated by the following execution sequence
3 state 1.1:
4 r1.state = 0
5 r2.state = 0
6 c.C1s = 0
7 c.C2s = 0
8 c.C1 = 0
9 c.C2 = 0
10
11 state 1.2:
12 c.C1s = 1
13
14 state 1.3:
15 c.C1s = 0
16 c.C2s = 1
17 c.C1 = 1
18
19 state 1.4:
20 r1.state = 1
21 c.C2s = 0
22 c.C1 = 0
23 c.C2 = 1
24
25 state 1.5:
26 r2.state = 1
27 c.C2 = 0
28
29 resources used:
30 processor time: 0 s,
31 BDD nodes allocated: 771
32 Bytes allocated: 1045224
33 BDD nodes representing transition relation: 78 + 1
FIG. 3.17: Verificação de Modelos para o programa de controle da manufatura(contra-exemplo).
54
saída C1 está desligada. O contato C1 é acionado, entretanto, no ramo precedente,
assim C2 poderia estar desligada mesmo que o valor da saída do controlador (como é
visto pela planta) possa ainda estar ligado. Conseqüentemente, o primeiro relé poderia
fazer uma transição para acionado e, ao final de um ciclo de varredura, o sinal C2 poderia
ser também acionado, colocando a planta em perigo durante a varredura seguinte, uma
vez que o relé R2 pode ser acionado em conjunto com R1.
C1
C2
C1s
C2s
r1.state
r2.state
1.1 1.2 1.3 1.4 1.5Estados
Local onde ocorre o problema
FIG. 3.18: Analise gráfica do contra-exemplo da especificação na linha 7 da Figura 3.16.
A solução para um controlador que evite este erro neste caso, é considerar os valores
velho e novo de C1 quando for computado o valor novo C2, conforme mostra a Figura
3.19 (RAUSCH & KROGH, 1998).
Após correção com base no contra-exemplo na Figura 3.17 e auxilio da análise gráfica
na Figura 3.18, a especificação passou a ser verdadeira conforme mostra a Figura 3.20.
55
FIG. 3.19: Projeto com base na análise do contra-exemplo.
1 -- specification AG (!r1.state | !r2.state) is true
2
3 resources used:
4 processor time: 0 s,
5 BDD nodes allocated: 323
6 Bytes allocated: 1045220
7 BDD nodes representing transition relation: 107 + 1
FIG. 3.20: Resposta da Verificação após correção do programa.
3.5 RESUMO DO CAPÍTULO
Neste capítulo é possível ter uma visão geral de como funciona a verificação de
modelos aplicada aos programas de CLP. Os programas são escritos na linguagem de
Diagramas de Contato. Porém um dos objetivos da dissertação é aplicar a verificação,
em programas de CLP escritos na linguagem de Diagrama de Blocos Funcionais (DBF).
O próximo capítulo trata da verificação aplicada a um sistema automatizado escrito
na linguagem DBF. São tratadas, ainda, estruturas mais complexas como memórias e
temporizadores.
56
4 CONTRIBUIÇÕES À APLICAÇÃO DA VERIFICAÇÃO DE MODELOS
AO PROJETO DE SISTEMAS AUTOMATIZADOS
O objetivo deste capítulo é aplicar as técnicas de verificação de modelos (model
checking) ao projeto de Sistemas Automatizados baseados em CLPs programados por
Diagramas de Blocos Funcionais (DBF). Foram desenvolvidos padrões para a verificação,
com base em estruturas lógicas típicas, visando uma futura automatização do processo.
4.1 PROJETO DE SISTEMAS AUTOMATIZADOS
A Figura 4.1 ilustra um modelo muito adotado por empresas de engenharia de au-
tomação para o projeto de sistemas automatizados. As etapas de um projeto são divididas
em quatro, a saber: elaboração de requisitos, projeto, implementação e teste e validação.
Na etapa de elaboração de requisitos as especificações do sistema são listadas. Alguns
documentos típicos produzidos nesta etapa são:
• Descritivos literais da automação;
• Padrões de lógica para sequenciamento e intertravamento;
• Matrizes de Causa e Efeito;
• Fluxogramas de Funcionamento, e
• Diagramas de Processo e Instrumentação.
Os padrões de lógica para sequenciamento seguem a norma ISA 5.2 (Diagramas
Lógicos Binários para Operações de Processos) (ISA, 1992).
Na etapa de projeto, com base nos documentos gerados pela etapa de elaboração
de requisitos, a própria empresa ou uma empresa terceirizada desenvolve o projeto do
sistema automatizado. Documentos típicos gerados nesta fase são:
• Mapa de Memória do CLP;
• Lista de Entradas e Saídas, e
• Listagem do Programa do CLP.
57
A listagem do programa segue o proposto pela norma IEC 61131-3. A maioria dos
programas gerados atualmente seguem os diagramas de contato. Para sistemas onde a
segurança é crítica, nota-se o emprego dos DBFs, que possuem um mapeamento direto
aos blocos da norma ISA 5.2.
Na fase de implementação, o diagrama desenvolvido é implementado no CLP corre-
spondente e montagens elétricas são realizadas. Novamente o processo pode ser terce-
irizado ou montado pela equipe de campo da contratante, com suporte da equipe que
elaborou o projeto.
Teste eValidação
Elaboração de Requisitos
Projeto
Implementação
FIG. 4.1: Método de projeto adotado por Empresas de Automação.
Na fase de testes e validação, são executados testes para comissionamento do sis-
tema. Tipicamente, testes de bancada ou os ditos loop-tests (testes feitos com o CLP
ligado à malha de controle) são realizados. Observa-se que estes testes não exaurem as
possibilidades de falha do sistema. Para alguns casos, o limite humano não possibilita a
visualização de certas falhas. Como a confiabilidade do sistema é garantida apenas pelos
testes, problemas não detectados podem causar prejuízos materiais, pessoais e ambien-
tais. Por outro lado, os erros detectados na fase de testes e validação acarretam o retorno
às fases anteriores, como ilustrado pelo tracejado na Figura 4.1. O retorno às etapas
anteriores corresponde a atrasos indesejáveis no cronograma do projeto.
58
4.2 EXEMPLO DE UM PROJETO DE SISTEMA AUTOMATIZADO
Para ilustrar o processo, toma-se como exemplo um projeto de uma chave de partida
estrela-triângulo (Y-△) para um motor trifásico. A finalidade de um sistema Y-△ em
um motor é de se reduzir a corrente de partida, ou seja, a corrente de pico no momento
da partida. É necessário que o motor seja do tipo de rotor em gaiola de esquilo, e todas
as pontas de ligação devem ser externas.
A tensão triângulo é a mesma da rede (será nesta tensão que o motor irá trabalhar).
A tensão em estrela (tensão de partida do motor) externamente ao motor também é a
mesma da triângulo, sendo menor nas bobinas do motor pelo tipo de ligação nos terminais.
4.2.1 DESCRIÇÃO LITERAL DAS ESPECIFICAÇÕES
A Figura 4.2 mostra o esquema elétrico do sistema estrela-triângulo. O funciona-
mento do sistema é o seguinte:
• Pressionando a botoeira L, as bobinas dos contactores K1, K3 (ligação em estrela)
são alimentadas, começando a contar o tempo programado;
• Após o tempo programado (10s), a alimentação da bobina de K3 é cortada, e a
bobina de K2 (ligação em triângulo) é acionada. As bobinas K1 e K2 são mantidas
energizadas;
• As contactoras K2 e K3 não podem estar acionadas ao mesmo tempo;
• Pressionando a botoeira D, desliga-se todo o sistema;
• Implementar a segurança de sobrecorrente com entrada de um contato do relé
térmico FT no CLP.
As entradas e saídas do sistema estão na Tabela 4.1.
4.2.2 MATRIZ DE CAUSA E EFEITO
A Matriz de Causa e Efeito (MCE) trata-se de uma tabela onde se estabelecem as
relações de seqüencialização de acionamento do sistema. Na primeira linha da tabela
listam-se os sinais que são as causas para os acionamentos, e na primeira coluna listam-se
os conseqüentes efeitos nos sinais do sistema. A Figura 4.3 ilustra a MCE para o processo
em questão.
59
FIG. 4.2: Sistema estrela-triângulo.
TAB. 4.1: Entradas e saídas do sistema
ENTRADASL Botoeira de liga (botão pulsante)D Botoeira de desliga (botão pulsante)FT Contato térmico
SAÍDASK1 Contactora de acionamentoK2 Contactora de acionamentoK3 Contactora de acionamento
L ac
iona
do
K1
acio
nado
K3
acio
nado
T >
10s
K3
desl
igad
o
D a
cion
ado
FT a
cion
ado
XX X XX X X
X X
Desliga K3
Liga K2
Desliga K1, K2 e K3
EFEITO
CA
US
A
Aciona K1 e K3
FIG. 4.3: Matriz de Causa e Efeito do sistema Y −△.
60
4.2.3 FLUXOGRAMA DE FUNCIONAMENTO E PROGRAMA DE APLICAÇÃO
A lógica de acionamento do programa de aplicação desenvolvido para este sistema é
demonstrada na forma de um Fluxograma na Figura 4.4.
L?
Aciona K1 e K3
T> 10s ?
Início
D?
!K3?
FT?
D?
Desliga K3
Aciona K2
FT?
S
S
N
N
S
D? FT?
S
Desliga K1, K2 e K3
N
N N
N
N
S S
S S
N
N
S
FIG. 4.4: Fluxograma para o sistema estrela-triângulo.
Neste trabalho está sendo mostrado o fluxograma pois é uma das maneiras utilizadas
pelas empresas para expressar a lógica de acionamento. Porém o uso do mesmo é arriscado
para Sistemas Industriais Automatizados, podendo induzir o projetista a inserir erros na
execução do projeto em DBF no CLP.
4.2.4 PROGRAMA EM DBF
A Figura 4.5 representa o programa escrito em diagramas de blocos funcionais DBF,
projetado por uma empresa de automação.
Supõe-se que os blocos utilizados são E (AND), OU (OR), memórias e tempo-
rizadores com atraso sincronizado (DI). A descrição detalhada do funcionamento dos
blocos encontra-se na Seção 4.5
61
FIG. 4.5: Programa em Diagramas de Blocos Funcionais.
4.3 PROPOSTA DE VERIFICAÇÃO DE MODELOS
Este trabalho tem como proposta inserir um método de verificação nas fases de
elaboração de requisitos e projeto do processo ilustrado na Figura 4.1, conforme mostrado
na Figura 4.6.
Na elaboração de requisitos, propõe-se um procedimento no qual faz-se a tradução de
especificações, para especificações em CTL. Já na fase de projeto, os programas escritos
em DBF no CLP são traduzidos no código reconhecido pela ferramenta de verificação. O
processo se fecha com uma etapa de verificação. O resultado da verificação, quando da
obtenção de um erro, é utilizado para refinamento dos requisitos e/ou reprojeto. Com
este processo objetiva-se aumentar a confiabilidade do sistema e minimizar o atraso no
projeto por erros detectados na fase de testes e validação.
Nas próximas seções, as etapas do processo de verificação são detalhadas.
62
Verificação
Módulo do prog.do CLP em SMV
Re-projeto
Refinamento dos requisitos
Elaboração de Requisitos
Projeto
Implementação
Teste eValidação
Especificação em CTL
FIG. 4.6: Procedimento atual e proposta de modificação.
4.4 ESCRITA DA ESPECIFICAÇÃO
O estudo feito para este trabalho mostra que existem duas maneiras de escrever as
especificações CTL para sistemas automatizados. Pode ser feita a partir da matriz de
causa e efeito, como apresentado na Seção 4.4.1 e também a partir do conhecimento do
sistema, como apresentado na Seção 4.4.2.
4.4.1 ESCRITA DE ESPECIFICAÇÕES A PARTIR DA MATRIZ DE CAUSA E
EFEITO
Este desenvolvimento consiste na obtenção de especificações CTL com base na MCE.
A Figura 4.7 ilustra a base do procedimento proposto para sistematização da escrita das
especificações CTL. Nesta figura:
• V AR representa uma variável de saída do sistema;
• CON representa as condições que levam a variável V AR assumir a condição 1 (equi-
valente a ON ou VERDADEIRO), denominada condição para verdadeiro;
• COFF representa as condições que levam a variável V AR assumir a condição 0
(equivalente a OFF ou FALSO), denominada condição para falso.
63
COFF
CONVARLógica
FIG. 4.7: Escrita de especificações CTL.
Exploram-se as informações a respeito do acionamento de variáveis na MCE para es-
crita de propriedades CTL. As especificações podem ser escritas de duas formas diferentes
em função do acionamento e do desligamento da variável V AR.
Para o acionamento da variável V AR escrevem-se duas especificações:
• A primeira especificação é:
AG(CON&!COFF− > AF(V AR)), (4.1)
a significar que sempre que a condição para verdadeiro for válida e a condição para
falso for não válida (CON&!COFF ) então, para todos os caminhos no futuro, V AR será
verdadeira.
• A outra especificação é:
AG(!V AR− >!E[!CONU(V AR&!CON)]), (4.2)
a significar que sempre que V AR passar de falso para verdadeiro, CON deve também ser
válida. Isso significa que V AR não passa para verdadeiro por qualquer outra condição
que não seja CON .
Para o desligamento da variável V AR escrevem-se também duas especificações:
• A primeira especificação é:
AG(COFF &!CON− > AF(!V AR)), (4.3)
a significar que sempre que a condição para falso for válida e a condição para verdadeiro
for não válida (COFF &!CON) então, para todos os caminhos no futuro, V AR será não
verdadeira.
• A outra especificação é:
64
AG(V AR− >!E[!COFFU(!V AR&!COFF )]), (4.4)
a significar que sempre que V AR passar de verdadeiro para falso, COFF deve também
ser válida. Isso significa que V AR não passa para falso por qualquer outra condição, a
não ser por COFF .
Baseado na Tabela 4.1 de entradas e saídas e na Matriz de Causa e Efeito do sistema
Y −△, são mostradas as condições para verdadeiro e falso para as variáveis K1, K2 e K3
na Tabela 4.2.
TAB. 4.2: Condições para representação das Saídas
SAÍDAS CON COFF
Contactora K1 L (D|FT)Contactora K2 (T1 & !K3) (D|FT)Contactora K3 (L & !K2) (D|FT|T1)
Para a contactora K1, a condição que a torna verdadeira é L e a que a torna falsa
é D ou FT. Já para a contactora K2, a condição que a torna verdadeira é T1, variável
binária a significar que o tempo em triângulo terminou, e !K3, e a que a torna falsa é D
ou FT. Da mesma forma, para a contactora K3, a condição que a torna verdadeira é L e
!K2, e a que a torna falsa é D ou FT ou T1.
De acordo com as especificações sistematizadas para o acionamento (especificações
4.1 e 4.2) e desligamento (especificações 4.3 e 4.4) de variáveis de saída, mostram-se as
especificações para o sistema Y −△ levando em conta as condições para verdadeiro e falso
descritas para cada uma das contactoras. Substituindo as condições de cada contactora
tem-se:
• As especificações para o acionamento de K1:
AG(L&!(D|FT )− > AF(K1)) (4.5)
AG(!K1− >!E[!LU(K1&!L)]) (4.6)
• Especificações para o desligamento de K1:
65
AG((D|FT )&!L− > AF(!K1)) (4.7)
AG(K1− >!E[!(D|FT )U(!K1&!(D|FT ))]) (4.8)
• Especificações para o acionamento de K2:
AG((T1&!K3)&!(D|FT )− > AF(K2)) (4.9)
AG(!K2− >!E[!(T1&!K3)U(K2&!(T1&!K3))]) (4.10)
• Especificações para o desligamento de K2:
AG((D|FT )&!(T1&!K3)− > AF(!K2)) (4.11)
AG(K2− >!E[!(D|FT )U(!K2&!(D|FT ))]) (4.12)
• Especificações para o acionamento de K3:
AG((L&!K2)&!(D|FT |T1))− > AF(K3)) (4.13)
AG(!K3− >!E[!(L&!K2)U(K3&!(L&!K2))]) (4.14)
• Especificações para o desligamento de K3 (4.15) e (4.16).
AG((D|FT |T1)&!(L&!K2)− > AF(!K3)) (4.15)
AG(K3− >!E[!(D|FT |T1)U(!K3&!(D|FT |T1))]) (4.16)
66
4.4.2 ESCRITA DAS ESPECIFICAÇÕES A PARTIR DO CONHECIMENTO DO SIS-
TEMA
Esta seção apresenta uma outra forma de especificação baseada no conhecimento do
sistema, subentendida por especificação estrutural.
Um primeiro tipo pode expressar segurança para o sistema, pela expressão AG p,
onde apresenta uma situação no qual a propriedade p sempre é válida para o sistema.
Para o sistema Y −△ pode-se representar essa especificação na forma:
AG!(K2&K3)
a representar que as saídas K2 e K3 não podem estar acionadas simultaneamente. Esse
tipo de especificação é expressa informalmente como nada bom/ruim vai acontecer.
Dois outros tipos de especificações estruturais podem ser escritas para uma dada
propriedade p: vivacidade, AF p, a significar que sempre a propriedade p será verdade no
futuro, informalmente expresso como algo bom/ruim vai acontecer, e alcançabilidade, EF
p , a significar que eventualmente a propriedade p será verdade no futuro, informalmente
expresso como algo bom/ruim pode acontecer (CLARKE et al., 1999).
4.5 A TRADUÇÃO DA LINGUAGEM DBF EM CÓDIGO SMV
Esta seção apresenta um método de tradução de um programa escrito em DBF para
o código do SMV. Com objetivo de uma automatização do método de tradução foram
desenvolvidos gabaritos de código SMV para as estruturas típicas da norma ANSI/ISA
5.2 (ISA, 1992).
4.5.1 ELEMENTOS DE LÓGICA BOOLEANA
A Figura 4.8 mostra os blocos de lógica básica que são utilizados na elaboração do
DBF. Essa figura é apresentada em três colunas as quais representam:
• A Figura 4.8(a): o bloco lógico E (AND). A variável de saída D é verdade se
somente se todas as variáveis de entra A, B e C forem verdade. Na linguagem
SMV escreve-se D:= A&B&C;
• A Figura 4.8(b): o bloco lógico OU (OR). A variável de saída D é verdade se so-
mente se uma ou mais variáveis de entrada A, B ou C forem verdade. Na linguagem
do SMV, escreve-se D:= A|B|C;
67
• A Figura 4.8(c): o bloco lógico NÃO (NOT ). A variável de saída B existe se somente
se a variável de entrada A for falsa. Na linguagem do SMV, escreve-se B:= !A;
FIG. 4.8: Blocos lógicos AND, OR e NOT.
4.5.2 ELEMENTOS DE MEMÓRIA
A Figura 4.9 mostra os blocos de memória no qual S representa SET e R representa
RESET. Na Figura 4.9 (a), a saída lógica C é verdade assim que a entrada lógica A seja
verdade. C continua a ser verdadeiro, indiferentemente do estado subseqüente de A, até
que a entrada lógica B seja verdade. C permanece no estado falso indiferentemente do
estado subseqüente de B, até que A volte a ser verdadeira. A saída lógica D (se usada),
é verdadeira quando C não for verdadeira, e D é falso quando C for verdadeiro. Se as
entradas S e R estiverem em simultaneidade, e se deseja que S tenha prioridade sobre
R, então S tem que ser circulado conforme apresentado em (a), e se R tem prioridade
sobre S, então R deve ser circulado conforme (b) da Figura 4.9.
FIG. 4.9: Blocos SET/RESET.
A Figura 4.10(a) ilustra o código correspondente aos blocos de memória com prior-
idade para SET e a Figura 4.10(b) ilustra o bloco com prioridade para RESET. Esse
código foi elaborado de acordo com a lógica booleana das memórias correspondentes.
68
FIG. 4.10: Códigos SET/RESET.
4.5.3 BLOCOS TEMPORIZADORES
A Figura 4.11 ilustra os blocos dos temporizadores que podem ser utilizados na
elaboração do DBF segundo norma ISA 5.2 (ISA, 1992). Essa figura é apresentada em
três colunas as quais representam:
• Figura 4.11(a): Bloco do Temporizador por atraso no acionamento (Delay Initiation
of Output - DI ). A permanência contínua da entrada lógica A em verdadeiro por
um tempo t causa uma saída lógica B verdadeira quando t termina. B volta a falso
quando A volta a falso.
• Figura 4.11(b): Bloco do Temporizador por atraso no desligamento (Delay Ter-
mination of Output - DT ). A passagem da entrada lógica A para verdadeiro, faz
a saída lógica B torna-se verdadeira imediatamente. B torna-se falsa quando A
torna-se falsa e permanecer neste estado por um tempo t.
• Figura 4.11(c): Bloco do Temporizador de tempo fixo (Pulse Output - PO). A
passagem da entrada lógica A para verdadeiro, indiferentemente do estado sub-
seqüente, faz saída lógica B tornar-se verdadeira imediatamente. B permanece
verdadeira por um tempo t, e então torna-se falsa.
Num modelo de um temporizador que leve em conta o passo-a-passo da contagem,
a variável de contagem do temporizador assume valores discretos que vão de zero ao
tempo final de contagem, numa quantidade dependente do passo de contagem. Numa
representação em estado discreto para um temporizador, o número de estados seria muito
grande, pois estes deveriam corresponder aos valores assumidos pela variável de contagem.
69
FIG. 4.11: Blocos dos temporizadores DI, DT, PO.
Para evitar esta complexidade na modelagem do temporizador. Trabalha-se com uma
abstração, como ilustram as Figuras 4.12, 4.13 e 4.14. Essas figuras mostram máquinas
de estado correspondentes aos temporizadores. A máquina de estado possui três estados
os quais variam de acordo com o tipo de temporizador utilizado. Os temporizadores
DI representado na Figura 4.12 (a) e PO na Figura 4.14 (a) são formados pelos estados
parado, contando e terminado. O temporizador DT na Figura 4.13 (a) é formado pelos
estados parado, contando e alto. Todos os estados e saídas dos temporizadores estão
ilustrados nas respectivas figuras sob a letra (b). Esses gráficos foram utilizados para
modelar os temporizadores e foram inspirados em IEC (2003).
FIG. 4.12: Máquinas de estado correspondente ao código do temporizador DI.
A Figura 4.15 ilustra os códigos correspondentes a cada um dos blocos dos tempo-
rizadores DI, DT e PO respectivamente, que são traduzidos de forma direta a partir das
respectivas máquinas de estado das Figuras 4.12, 4.13 e 4.14.
70
FIG. 4.13: Máquinas de estado correspondente ao código do temporizador DT.
FIG. 4.14: Máquinas de estado correspondente ao código do temporizador PO.
71
FIG. 4.15: Códigos dos temporizadores.
4.5.4 CONSTRUÇÃO MODULAR DO CÓDIGO
O código para verificação no SMV é construído modularmente a partir do programa
em DBF por interligação dos carimbos correspondentes aos blocos do diagrama.
A Figura 4.16 ilustra as variáveis definidas para os blocos do programa na Figura 4.5.
São definidas as variáveis Q1, Q2, Q3, e Q5 (memórias) e temp (temporizador DI). Uma
importante consideração é como se processa a varredura do programa. Assume-se que a
varredura é da esquerda para direita e de cima para baixo dos blocos. Assim, deve-se
tomar cuidado na hora de modelar as variáveis que voltam em linhas da direita para a
esquerda para alimentar os outros blocos.
72
FIG. 4.16: Programa em Diagramas de Blocos Funcionais com as variáveis auxiliares.
A Figura 4.17 mostra como é o processo de modularização do sistema utilizando os
carimbos para a tradução do diagrama da Figura 4.5 em código SMV . Como se pode ob-
servar, a seqüência dos módulos do programa são declarados a partir do módulo principal
main na linha 1, com as variáveis de entradas booleanas nas linhas 2 a 5 e a instância
do programa na linha 6. Definem-se as saídas como K1, K2, K3 e T1 nas linhas 7 a 11
do programa. Em seguida, nas linhas de 12 a 13, colocam-se as especificações do sistema
na linguagem CTL. Nas linhas 14 a 19 são implantados os códigos dos temporizadores
e memórias que, para o exemplo, utilizam-se apenas o temporizador DI (mostrado) e as
memórias com prioridade para SET e para RESET (não mostrados). A colocação dos
blocos de memória, temporizadores e outros não precisa ser necessariamente nessa ordem.
Para finalizar, faz-se o módulo do programa ser verificado, onde se encontra a lógica
de seqüenciamento nas linhas 20 a 26 de acordo com o programa escrito em DBF na
Figura 4.16. Consideram-se as saídas correspondentes aos blocos de memória do projeto
como saídas Q1, Q2, Q3, uma saída auxiliar Qs e a saída do temporizador temp. Depois
definem-se essas saídas como K1, K2, K3 e T1 nas linhas 27 a 31 do programa principal
para facilitar a interpretação da resposta da verificação.
É importante observar que a saída do bloco do temporizador DI retorna aos blocos
de memória Q2 e Q3 na Figura 4.16. Em conseqüência, é necessário não utilizar o next na
interligação dos blocos do temporizador nas linhas 23 e 24 da Figura 4.17, pois se pode
omitir erros na verificação devido a consideração de que a varredura do CLP se processa
73
da esquerda para a direita do diagrama.
1 MODULE main
2 VAR
3 L : boolean;
4 D : boolean;
5 FT : boolean;
6 c : programa_empresa(L,D,FT);
7 DEFINE
8 K1:= c.K1;
9 K2:= c.K2;
10 K3:= c.K3;
11 T1:= c.T1;
12 SPEC AG (L & !(D|FT) -> AF K1)
13 ...
14 MODULE DI(entrada)
15 ...
16 MODULE resetset(entrada_set,entrada_reset)
17 ...
18 MODULE setreset(entrada_set,entrada_reset)
19 ...
20 MODULE programa_empresa(L,D,FT)
21 VAR
22 Q1 : setreset(L,(D|FT));
23 Q2 : setreset((temp.saida & !next(Q3.saida)),(D|FT));
24 Q3 : setreset(L,(D|FT) | temp.saida);
25 Qs : setreset(L,(D|FT));
26 temp : DI(next(Qs.saida));
27 DEFINE
28 K1:= Q1.saida;
29 K2:= Q2.saida;
30 K3:= Q3.saida;
31 T1:= temp.saida;
FIG. 4.17: Tradução do DBF em código SMV.
4.6 VERIFICAÇÃO
A verificação é uma etapa que informa se o sistema está de acordo com as especi-
ficações ou não, neste caso, informa-se um contra-exemplo. Um contra-exemplo é uma
seqüência de ações tomadas pelo programa de controle que viola as especificações. Para
as especificações das linhas 7, 10 e 13 na Figura 4.18, ocorre uma violação do programa
projetado (programa_empresa na linha 20 da Figura 4.17) com as especificações dese-
jadas. A Figura 4.18 mostra o resultado da verificação. As linhas 1 a 6, 8, 9, 11 e 12
mostram que o programa não viola as respectivas especificações, descrevendo que são
verdadeiras. Em conseqüência da violação, o SMV proporciona um contra-exemplo das
especificações que foram falsas, como mostrado nas Figuras 4.19, 4.20 e 4.21.
74
1 -- specification AG (L & !(D | FT) -> AF K1) is true
2 -- specification AG (!K1 -> !E((!L) U (K1 & !L))) is true
3 -- specification AG ((D | FT) & !L -> AF (!K1)) is true
4 -- specification AG (K1 -> !E((!(D | FT)) U (!K1 & !(D | ... is true
5 -- specification AG (T1 & !K3 & !(D | FT) -> AF K2) is true
6 -- specification AG (!K2 -> !E((T1 & !K3) U (K2 & T1 & !K... is true
7 -- specification AG ((D | FT) & !(T1 & !K3) -> AF (!K2)) is false
8 -- specification AG (K2 -> !E((!(D | FT)) U (!K2 & !(D | ... is true
9 -- specification AG (L & !K2 & !(D | FT | T1) -> AF K3) is true
10 -- specification AG (!K3 -> !E((!(L & !K2)) U (K3 & !(L &... is false
11 -- specification AG ((D | FT | T1) & !L -> AF (!K3)) is true
12 -- specification AG (K3 -> !E((!(D | FT | T1)) U (!K3 & !... is true
13 -- specification AG (!(K2 & K3)) is false
FIG. 4.18: Resposta da verificação.
75
1 -- specification AG ((D | FT) & !(T1 & !K3) -> AF (!K2)) is false
2 -- as demonstrated by the following execution sequence
3 state 1.1:
4 T1 = 0
5 K3 = 0
6 K2 = 0
7 K1 = 0
8 L = 0
9 D = 0
10 FT = 0
11
12 state 1.2:
13 L = 1
14
15 state 1.3:
16 K3 = 1
17 K1 = 1
18 L = 0
19 c.temp.estado = contando
20
21 state 1.4:
22 T1 = 1
23
24 state 1.5:
25 K3 = 0
26 K2 = 1
27 L = 1
28 -- loop starts here --
29 state 1.6:
30 K3 = 1
31 L = 0
32 FT = 1
33 state 1.7:
34 T1 = 0
35 K3 = 0
36 K1 = 0
37 L = 1
38 FT = 0
39
40 state 1.8:
41 K3 = 1
42 K1 = 1
43 L = 0
44 c.temp.estado = contando
45
46 state 1.9:
47 T1 = 1
48 FT = 1
FIG. 4.19: Contra-exemplo da especificação na linha 7 da Figura 4.18.76
1 -- specification AG (!K3 -> !E((!(L & !K2)) U (K3 & !(L &... is false
2 -- as demonstrated by the following execution sequence
3 state 2.1:
4 T1 = 0
5 K3 = 0
6 K2 = 0
7 K1 = 0
8 L = 0
9 D = 0
10 FT = 0
11
12 state 2.2:
13 L = 1
14
15 -- loop starts here --
16 state 2.3:
17 K3 = 1
18 K1 = 1
19 L = 0
20
21 state 2.4:
22 T1 = 1
23 FT = 1
24
25 state 2.5:
26 T1 = 0
27 K3 = 0
28 K2 = 1
29 K1 = 0
30 FT = 0
31
32 state 2.6:
33 L = 1
34 FT = 1
35
36 state 2.7:
37 K3 = 1
38 K2 = 0
39 K1 = 1
40 L = 0
41 FT = 0
FIG. 4.20: Contra-exemplo da especificação na linha 10 da Figura 4.18.
77
1 -- specification AG (!(K2 & K3)) is false
2 -- as demonstrated by the following execution sequence
3 state 3.1:
4 T1 = 0
5 K3 = 0
6 K2 = 0
7 K1 = 0
8 L = 0
9 D = 0
10 FT = 0
11
12 state 3.2:
13 L = 1
14
15 state 3.3:
16 K3 = 1
17 K1 = 1
18 L = 0
19
20 state 3.4:
21 T1 = 1
22
23 state 3.5:
24 K3 = 0
25 K2 = 1
26 L = 1
27
28 state 3.6:
29 K3 = 1
30 L = 0
FIG. 4.21: Contra-exemplo da especificação na linha 13 da Figura 4.18.
4.6.1 REPROJETO
Para a especificação da linha 7 da Figura 4.18 o contra-exemplo na Figura 4.19
ilustra um traço de erro do programa. Analisando o contra-exemplo pode-se ver que no
estado 1.9 da linha 46 ocorre a proteção de sobrecorrente através do relé térmico (FT)
e a prioridade para SET não impõe o desligamento geral do sistema, ocasionando uma
falha.
Para a especificação da linha 10 da Figura 4.18, o contra-exemplo na Figura 4.20
mostra que no estado 2.6 na linha 32 o sistema Y −△ e o relé térmico (L = 1 e FT = 1)
acionam simultaneamente. O sistema Y − △ continua ativo e a prioridade é para o
sistema desligar devido à proteção do relé térmico.
78
Por fim a especificação da linha 13 da Figura 4.18. O contra-exemplo na Figura
4.21 mostra um traço de erro que no estado 3.5, na linha 23, ocorre um erro devido ao
religamento do sistema estando K1 e K2 ainda ativos. O religamento do sistema faz com
que K3 seja ativado no estado 3.6 na linha 28. Porém, sendo prioridade para SET, K3
fica ativo em simultaneidade com K2.
Após a análise dos traços de eventos, é possível modificar o programa de aplicação
para que estes traços sejam suprimidos, o que corresponde a etapa de reprojeto. A partir
dos contra-exemplos identificam-se que a inserção dos blocos de memória com prioridade
SET violam as especificações e o correto é a prioridade RESET. O sistema reprojetado
está na Figura 4.22. A posterior verificação para o reprojeto na Figura 4.23 indicou que
todas as especificações da Figura 4.18 são verdadeiras para o sistema reprojetado.
FIG. 4.22: Reprojeto com base no contra-exemplo.
79
1 MODULE programa_reprojeto(L,D,FT)
2 VAR
3 Q1 : resetset(L,(D|FT));
4 Q2 : resetset((temp.saida & !next(Q3.saida)),(D|FT));
5 Q3 : resetset(L,(D|FT) | temp.saida);
6 Qs : resetset(L,(D|FT));
7 temp : DI(next(Qs.saida));
8 DEFINE
9 K1:= Q1.saida;
10 K2:= Q2.saida;
11 K3:= Q3.saida;
12 T1:= temp.saida;
FIG. 4.23: Reprojeto na linguagem SMV.
4.7 RESUMO DO CAPÍTULO
Este capítulo tem como contribuições a criação de um procedimento de tradução
de processos escrito em DBF para um código aceito pelo SMV. Tratam-se da sistem-
atização de padrões na tradução da MCE e em especificações na linguagem CTL e da
inserção da verificação no projeto de sistemas automatizados escritos na linguagem DBF.
Uma vantagem em relação a abordagens semelhantes é a busca pela sistematização dos
procedimentos de verificação, visando futuro automatismo do processo.
80
5 APLICAÇÃO NA AUTOMAÇÃO DE UM AQUECEDOR A CHAMA
Este capítulo mostra a aplicação da verificação de modelos ao projeto de automação
de um Aquecedor a Chama (API, 1997). Trata-se em particular da automação do processo
de purga, etapa da inicialização do aquecedor (API, 1997). Os documentos de projeto
analisados na verificação são a descrição literal das especificações, a matriz de causa e
efeito e o programa em DBF, escrito segundo a norma ISA 5.2 (ISA, 1992).
5.1 AUTOMAÇÃO DO PROCESSO DE PURGA
Nesta seção descreve-se a documentação do projeto da automação do processo de
purga de um aquecedor a chama (API, 1997).
5.1.1 SEQÜÊNCIA DE PURGA
O processo de purga do aquecedor consiste nos seguintes passos:
a) Para iniciar a seqüência, o sinal Permissão de Purga deve estar ativo;
b) O operador comanda Iniciar Purga;
c) A válvula de vapor deve ser aberta automaticamente, e a indicação Purga em An-
damento deve começar a piscar quando a chave de fim-de-curso ZSH-XV-VAPOR
confirmar a abertura total da válvula;
d) Uma vez que a indicação de Purga em Andamento é observada, um temporizador
deve ser iniciado, e o tempo de purga deve começar. O tempo de purga deve ser
T1;
e) Se o operador fecha a válvula de vapor antes do tempo total de purga ou, se o
operador comandar Desistência de Purga, a seqüência de inicialização deve ser
inibida e uma nova purga será necessária para habilitar qualquer ignição;
f) Se qualquer intertravamento que cause o desligamento geral do aquecedor a chama
é disparado durante a operação de purga, a seqüência de inicialização deve ser
abortada e, após o término da operação de purga, a ignição não será permitida;
81
g) O fechamento da válvula de vapor após o tempo de purga será automático, e a
indicação Permissão para Ignição piscará durante T2.
5.1.2 LISTA DE ENTRADAS E SAÍDAS
As Tabelas 5.1 e 5.2 apresentam a correspondência lógica de entradas e saídas.
Considera-se que todas as variáveis são binárias, assumindo os valores 0 (equivalente
a falso ou off ) e 1 (equivalente a verdadeiro ou on).
TAB. 5.1: Variáveis de entrada do sistema
Sensores/Sinais de entrada Variável Correspondência lógica
Permissão de Purga perm_purg habilitada = 1Iniciar Purga init_purg acionado = 1
Chave ZSH-XV-VAPOR fch_xv acionada = 1Desistência de Purga des_purg acionado = 1
Intertravamento para desligamento do purga sd_purg acionado = 1
TAB. 5.2: Variáveis de saída do sistema
Atuadores/Indicadores Variável Correspondência lógica
Abertura da válvula de vapor abre_xv para abrir = 1Purga em Andamento indic_purg acionado = 1Permissão para Ignição indic_ignit acionada = 1
5.1.3 MATRIZ DE CAUSA E EFEITO
A Figura 5.1 mostra a Matriz de Causa e Efeito para o sistema descrito anteriormente.
82
init_
purg
perm
_pur
g
! des
_pur
g
! sd_
purg
fch_
xv
T1 des_
purg
sd_p
urg
T2
Com
ando
de
Inic
iar
Purg
a
Sin
al d
e Pe
rmis
são
de P
urga
Ope
rado
r nã
o C
oman
da
Des
istê
ncia
de
Purg
a
Não
aco
ntec
er In
tert
rava
men
to
SD
-PU
RG
A
Cha
ve d
e fim
-de-
curs
o Z
SH
-XV
-V
APO
R
Purg
a Fi
naliz
ada
Com
ando
de
desi
stên
cia
de
Purg
a
Inte
rtra
vam
ento
SD
-PU
RG
A
Igni
ção
Fina
lizad
a
Abre válvula de vapor abre_xv X X X XIndicação de Purga em Andamento indic_purg X X XIndicação Permissão para Ignição indic_ignit XFecha válvula de vapor ! abre_xv X XFim da Indicação de Purga em Andamento ! indic_purg X X XFim da Indicação de Permissão para Ignição ! indic_purg X X
CA
US
A
EFEITO
FIG. 5.1: Matriz de Causa e Efeito do sistema Purga.
Na matriz de causa e efeito da Figura 5.1, T1 e T2 são variáveis binárias que indicam
o término dos tempos de purga e ignição respectivamente (T1, T2=1 equivale ao término
da contagem).
5.1.4 PROJETO DO PROGRAMA EM DBF
Na Figura 5.2 está o projeto de automação do sistema Purga do Aquecedor a Chama
escrito na linguagem DBF. A interpretação dos símbolos segue a norma ISA 5.2 (ISA,
1992), alguns símbolos adicionais são apresentados na Figura 5.3.
83
FIG. 5.2: Projeto do sistema Purga.
FIG. 5.3: Tipos de sinal, segundo a norma ISA 5.2 (ISA, 1992).
5.2 MODELAGEM DAS ESPECIFICAÇÕES
As condições para verdadeiro e falso da variável abre_xv estão nas equações abaixo.
CON = init_purg (5.1)
COFF = (T1|des_purg|sd_purg|!perm_purg|indic_ignit) (5.2)
A condição para verdadeiro da variável abre_xv é que o operador comande o início de
purga (init_purg). A condição para falso da variável abre_xv é ou que o tempo de purga
84
termine (T1), ou que o operador comande a desistência de purga (des_purg), ou que haja
um intertravamento para desligamento da purga (sd_purg), ou que a permissão de purga
seja desabilitada (!perm_purg), ou que a ignição esteja em andamento (indic_ignit).
As condições para verdadeiro e falso da variável indic_purg estão abaixo:
CON = (fch_xv&abre_xv) (5.3)
COFF = (des_purg|sd_purg|T1|!perm_purg|!fch_xv) (5.4)
A condição para verdadeiro da variável indic_purg é que a chave de fim-de-curso
confirme a abertura total da válvula (fch_xv) e esteja ativo o comando da abertura da
válvula de vapor (abre_xv). A condição para falso da variável indic_purg é ou que
exista desistência de purga (des_purg), ou intertravamento da purga (sd_purg), ou que
o tempo de purga termine (T1), ou que não exista permissão de purga (!perm_purg), ou
que o operador feche manualmente a válvula de vapor (!fch_xv).
As condições para verdadeiro e falso da variável indic_ignit são:
CON = T1 (5.5)
COFF = (sd_purg|T2) (5.6)
A condição para verdadeiro da variável indic_ignit é que o tempo de purga termine
(T1). A condição para falso da variável indic_ignit é ou que exista intertravamento da
purga (sd_purg), ou que o tempo de ignição termine (T2).
De acordo com as especificações sistematizadas para o acionamento (especificações
4.1 e 4.2) e desligamento (especificações 4.3 e 4.4), desenvolvem-se as especificações para
o sistema.
• As especificações de acionamento para abre_xv:
AG((init_purg&!(T1|des_purg|sd_purg|!perm_purg|indic_ignit)− > AF(abre_xv))
(5.7)
AG(!abre_xv− >!E[!init_purgU(abre_xv&!init_purg)]) (5.8)
85
• Especificações de desligamento para abre_xv:
AG((T1|des_purg|sd_purg|!perm_purg|indic_ignit)&!init_purg− > AF(!abre_xv))
(5.9)
AG(abre_xv− >!E[!(T1|des_purg|sd_purg|!perm_purg|indic_ignit)U(!abre_xv&
!(T1|des_purg|sd_purg|!perm_purg|indic_ignit))]) (5.10)
• Especificações de acionamento para indic_purg:
AG((fch_xv&abre_xv)&!(des_purg|sd_purg|T1|!perm_purg|!fch_xv)− >
AF(indic_purg)) (5.11)
AG(!(indic_purg)− >!E[!(fch_xv&abre_xv)U(indic_purg&!(fch_xv&abre_xv))])
(5.12)
• Especificações de desligamento para indic_purg:
AG((des_purg|sd_purg|T1|!perm_purg|!fch_xv)&!(fch_xv&abre_xv)− >
AF(!indic_purg)) (5.13)
AG(indic_purg− >!E[!(des_purg|sd_purg|T1|!perm_purg|!fch_xv)U
(!indic_purg&!(des_purg|sd_purg|T1|!perm_purg|!fch_xv))]) (5.14)
• Especificações de acionamento para indic_ignit:
AG(T1&!(sd_purg|T2)− > AF(indic_ignit)) (5.15)
AG(!(indic_ignit)− >!E[!T1U(indic_ignit&!T1)]) (5.16)
86
• Especificações de desligamento para indic_ignit:
AG((sd_purg|T2)&!T1− > AF(!indic_ignit)) (5.17)
AG(indic_ignit− >!E[!(sd_purg|T2)U(!indic_ignit&!(sd_purg|T2))]) (5.18)
Além das especificações acima, baseado no conhecimento do sistema, são expressas
situações indesejadas para o projeto (especificações de segurança). Para o sistema purga
foram identificadas três situações que não podem ocorrer, listadas abaixo.
• A especificação na equação 5.19 expressa que não pode ocorrer indicação de Purga
em Andamento (indic_purg) com a válvula de vapor fechada (!fch_xv):
AG!(indic_purg&!fch_xv) (5.19)
• A especificação na equação 5.20 expressa que não pode ocorrer a não permis-
são de purga (!perm_purg) seguida do comando de abrir a válvula de vapor
(AX(abre_xv)):
AG!(!perm_purg&AX(abre_xv)) (5.20)
• A especificação na equação 5.21 expressa que não pode estar a purga desabilitada
(!(perm_purg)) e, em seguida, ocorrer a indicação de purga em andamento (in-
dic_purg):
AG!(!perm_purg&AX(indic_purg)) (5.21)
5.3 MODELAGEM DO PROGRAMA
Na Figura 5.4, reproduz-se a Figura 5.2 com inserção de variáveis auxiliares para
modelagem de programa no SMV. A Figura 5.5 representa a modelagem do sistema
purga utilizando os carimbos correspondentes aos blocos do diagrama da Figura 5.4.
O módulo principal main é composto pelas variáveis de entrada booleanas nas linhas
2 a 7, seguida da representação das saídas Q1, Q2, temp1 e temp2 nas linhas 9 a 13,
87
representadas como instâncias dos módulos definidos nas linhas 24 a 27. Depois são
representadas as especificações do sistema, seguidas dos módulos dos blocos temporizador
e memória.
FIG. 5.4: Projeto do sistema Purga com inserção de variáveis auxiliares.
88
1 MODULE main
2 VAR
3 perm_purg : boolean;
4 init_purg : boolean;
5 fch_xv : boolean;
6 des_purg : boolean;
7 sd_purg : boolean;
8
9 Q1 : resetset(init_purg,(Q2.saida|!perm_purg|sd_purg|des_purg));
10 Q2 : resetset(next(temp1.saida),(sd_purg|temp2.saida));
11
12 temp1 : DI(next(Q1.saida) & fch_xv);
13 temp2 : DI(next(Q2.saida));
14
15 DEFINE
16 abre_xv:= Q1.saida;
17 indic_purg:= Q1.saida & fch_xv;
18 indic_ignit:= Q2.saida;
19 T1:= temp1.saida;
20 T2:= temp2.saida;
21
22 SPEC AG !(indic_purg & !fch_xv)
23 ...
24 MODULE DI(entrada)
25 ...
26 MODULE resetset(entrada_set,entrada_reset)
27 ...
FIG. 5.5: Modelo do Programa no SMV.
5.4 VERIFICAÇÃO
Após a modularização do sistema é feita a verificação com as especificações descritas
na Seção 5.2. O resultado da verificação é mostrado na Figura 5.6. Observa-se que
todas as especificações são verdadeiras. Isso quer dizer que não ocorre uma violação das
especificações por parte do programa de automação da Purga projetado.
89
1 -- specification AG (init_purg & !(T1 | des_purg | sd_pur... is true
2 -- specification AG (!abre_xv -> !E((!init_purg) U (abre_... is true
3 -- specification AG ((T1 | des_purg | sd_purg | !perm_pur... is true
4 -- specification AG (abre_xv -> !E((!(T1 | des_purg | sd_... is true
5 -- specification AG (fch_xv & abre_xv & !(des_purg | sd_p... is true
6 -- specification AG (!indic_purg -> !E((!(fch_xv & abre_x... is true
7 -- specification AG ((des_purg | sd_purg | T1 | !perm_pur... is true
8 -- specification AG (indic_purg -> !E((!(des_purg | sd_pu... is true
9 -- specification AG (T1 & !(sd_purg | T2) -> AF indic_ign... is true
10 -- specification AG (!indic_ignit -> !E((!T1) U (indic_ig... is true
11 -- specification AG ((sd_purg | T2) & !T1 -> AF (!indic_i... is true
12 -- specification AG (indic_ignit -> !E((!(sd_purg | T2)) ... is true
13 -- specification AG (!(indic_purg & !fch_xv)) is true
14 -- specification AG (!(!perm_purg & AX abre_xv)) is true
15 -- specification AG (!(!perm_purg & AX indic_purg)) is true
FIG. 5.6: Resposta da verificação do sistema Purga.
5.5 RESUMO DO CAPÍTULO
Este Capítulo mostra a importância da aplicação da verificação de modelos aos Sis-
temas Industriais Automatizados. Embora o projeto apresentado esteja correto, é impor-
tante observar que a modularização e sistematização proposta no trabalho mostra que o
tempo gasto para a validação do projeto é pequeno, podendo melhorar com a automatiza-
ção da verificação. Não foi preciso interromper, parar ou transferir nenhum processo em
campo para testar o programa do CLP, ao mesmo tempo que se aumenta a confiabilidade
inerente ao projeto.
90
6 CONCLUSÃO
Neste capítulo é apresentado um resumo, do ponto de vista metodológico, das con-
tribuições desta dissertação. São descritas as contribuições, assim como as perspectivas
para futuros estudos, baseados na experiência adquirida durante o desenvolvimento deste
trabalho.
6.1 CONTRIBUIÇÕES À VERIFICAÇÃO DE MODELOS
O Capítulo 4 apresenta as contribuições deste trabalho para a sistematização de
processos de Sistemas Industriais Automatizados.
Inicialmente é apresentada uma técnica de sistematização na tradução de especifi-
cações escritas a partir da MCE. Este procedimento se baseia em determinar as condições
que levam uma variável de saída a assumir uma condição verdadeira ou falsa. Isso quer
dizer, condições de acionamento e desligamento de variáveis de saída. Duas maneiras sis-
tematizadas para descrever especificações de desligamento foram criadas. Uma implica
em condições que podem ocorrer para o acionamento ou desligamento das variáveis e a
outra representa a obrigatoriedade de apenas determinadas condições levarem as variáveis
de saída a se tornarem falsas ou verdadeiras.
Outros tipos sistematizados de especificações são baseadas no conhecimento do sis-
tema. Estes tipos podem expressar a segurança, a alcançabilidade e a vivacidade do
sistema. Mostram sempre o comportamento das variáveis de saída.
Uma outra contribuição é a criação de um método de tradução de sistemas escritos
em DBF para o código SMV. Foram desenvolvidos gabaritos de códigos SMV para estru-
turas típicas da Norma ANSI/ISA 5.2. Sistematizou-se o procedimento incluindo desde
estruturas lógicas básicas até estruturas mais complexas, como elementos de memória e
blocos temporizadores. Tais blocos possuem correspondentes equivalentes na linguagem
DBF definidas na norma para programação de CLP IEC 61131-3 (IEC, 2003).
Criou-se também um procedimento para a construção modular do código para a
verificação no SMV.
A verificação dos sistemas Y − △ e Purga, mostraram a eficiência do reprojeto
orientado pelo traço de eventos do erro fornecido pelo SMV. Em muitos casos, entretanto,
a especificação testada mostrou-se uma propriedade falsa verdadeira, sendo muito restrita
91
para o sistema, obrigando a uma reescrita da mesma.
No Capítulo 5, demonstra-se a aplicabilidade do método proposto ao se abordar um
projeto de automação realista da etapa de purga de um aquecedor a chama.
Uma vantagem, em relação a abordagens anteriores, é a busca pela sistematização
dos procedimentos de verificação, visando um futuro automatismo do processo.
A fase de desenvolvimento do trabalho deu origem a dois artigos, o OLIVEIRA et al.
(2006b) apresenta a aplicação da verificação a sistemas instrumentados de segurança e o
OLIVEIRA et al. (2006a) a sistematização dos procedimentos de verificação de modelos
aplicada aos sistemas industriais automatizados controlados por CLP.
6.2 LIMITAÇÕES DA ABORDAGEM
Um problema na verificação de modelos utilizando a ferramenta SMV é que, depen-
dendo da quantidade de variáveis de entrada para determinadas especificações, o SMV
não mostra o contra-exemplo, apenas descreve que o programa não está de acordo com
a especificação. Isso é uma falha da ferramenta e pode ser corrigido por uso de outras
ferramentas.
Para tratamento de sistema de grande porte é necessário que seja feito algum tipo
de decomposição estrutural do processo, para que seja tratável pela ferramenta de verifi-
cação. Este ponto ainda está em desenvolvimento na pesquisa da verificação de modelos
(CLARKE et al., 1999).
O método funcionou bem para sistemas com um temporizador ou onde não há ne-
cessidade de verificar o funcionamento paralelo de dois temporizadores distintos. Neste
caso, dever-se-ia buscar uma ferramenta de verificação que tratasse do tempo explicita-
mente, como os autômatos temporizados tratados no HyTech (HENZINGER et al., 1997),
CheckMate (CHUTINAN, 1999) ou UPAAL (DAVID & LARSEN, 2004).
6.3 PERSPECTIVAS
Com relação aos estudos apresentados neste trabalho, existem alguns pontos que
merecem atenção e que representam possibilidades de trabalhos futuros.
Os códigos criados para a representação do programa DBF na linguagem SMV, não
foram retirados do código fonte do CLP, mas sim da sua lógica abstraída em máquinas
de estado. Portanto, um passo adicional interessante seria uma ferramenta que extraísse
o modelo a ser verificado diretamente do programa do CLP.
92
Foi desenvolvido um procedimento de verificação de programas de CLP modular, mas
esse procedimento não é automatizado. Não se tem conhecimento de uma ferramenta
computacional para verificação com tal funcionalidade.
93
7 REFERÊNCIAS BIBLIOGRÁFICAS
ALIPERTI, J. Gerenciamento de Alarmes: uma Situação Alarmante. Brasil InTech, (70):18–21, Abril 2005.
API. Instrumentation and Control Systems for Fired Heaters and Steam Gen-erators. API Recommended Practice 556, Maio 1997.
BRYANT, R. E. e MUSGRAVE, G. Panel: User Experience with High LevelFormal Verification. Em Design Automation Conference, pág. 327, 1998.
CADENCE. Cadence SMV - Symbolic model checker. http://www.kenmcmil.com/,junho 2002.
CAVADA, R. e CIMATTI, A. NuSMV version 2.2. [email protected], Novembro 2004.
CHUTINAN, A. Hybrid System Verification Using Discrete Model Approxima-tions. www.cs.cmu.edu/ webk/checkmate, Novembro 1999.
CLARKE, E. M. e EMERSON, E. A. Design and synthesis of synchronizationskeletons using branching time temporal logic. Em In Logic of Programs: work-shop, Yorktown Heights, NY, Maio 1981.
CLARKE, E. M., EMERSON, E. A. e SISTLA, A. P. Automatic verification offinite-state concurrent systems using temporal logic specifications. ACMTransactions on Programming Languages and Systems, 8(2):244–263, 1986.
CLARKE, E. M., GRUMBERG, O., HIRAISHI, H., JHA, S., LONG, D. E., MCMILLAN,K. L. e NESS, L. A. Verification of the Futurebus + cache coherence protocol.Em Claesen, 1993.
CLARKE, E. M., GRUMBERG, O. e PELED, D. A. Model Checking. The MIT Press,Cabridge, Massachusetts 02142, 1st edition, 1999.
CMU. The SMV system* for SMV: Version 2.5.4. www.cs.cmu.edu/ mod-elcheck/smv.html, Novembro 2000.
DAVID, G. e LARSEN, K. G. A Tutorial on UPPAAL: Formal Methods for theDesign of Real-Time Systems. International School on Formal Methods for theDesign of Computer, Comunication, and Software Systems, Nevembro 2004.
DIAS, C. A. Técnicas Avançadas de Instrumentação & Controle de ProcessosIndustriais. Editora e Gráfica ao Livro Técnico, [email protected], 1a edition, 2005.
FABIAN, M. e HELLGREN, A. PLC-based Implementation of Supervisory Con-trol for Discrete Event Systems. Em IEEE Conference on Decision and Control,págs. 16–18, Tampa, Florida, USA, Dezembro 1998.
94
FALCIONE, A. e KROGH, B. H. Design Recovery for Relay Ladder Logic. IEEETransactions on Automatic Control, 13(2):90–98, abril 1993.
GIBBS, W. W. Software’s Chonic Crisis. Scientific American, págs. 86–95, Setembro1994.
HENZINGER, T. A., HO, P. H. e WONG-TOI, H. HyTech: A Model Checker forHybrid Systems. Software tools for Technology Transfer, 1997.
HUGUES, G. E. e CRESWELL, M. J. Introduction to Modal Logic. Methuen, 1977.
IEC. Specification Language GRAFCET for Sequential Function Charts. IECInternational Standard 60848, Fevereiro 1999.
IEC. Programmable controllers−Part3: Programming languages. IEC Interna-tional Standard 61131 − 3, Janeiro 2003.
ISA. Binary Logic Diagrams for Process Operations ANSI/ISA 5.2. ISA-TheInstrumentation, Systems, and Automation Society, Julho 1992.
LAMPÉRIÈRE-COUFFIN, S., ROSSI, J.-M. e LESSAGE, J. Formal Validation ofPLC Programs : A Survey. University Laboratory in Automated Production Re-search, Julho 1999.
LONG, D. E. Model Checking, Abstration, and Compositional Reasoning. Tese(doutorado), Carnegie Mellon University, USA, 1993.
MCMILLAN, K. L. Symbolic Model Checking: An Approach to the State Ex-plosion Problem. Tese (doutorado), Carnegie Mellon University, USA, novembro1993.
MOON, I. Modeling Programmable Logic Controllers for Logic Verification.IEEE Transactions on Automatic Control, 14(2):53–59, Abril 1994.
OLIVEIRA, C. H. C., CUNHA, A. E. C. e CAMPOS, M. C. M. M. Verificação de Mo-delos Aplicada aos Sistemas Industriais Automatizados por ControladoresLógicos Programáveis. CBA Congresso Brasileiro de Automática, Outubro 2006a.
OLIVEIRA, C. H. C., CUNHA, A. E. C. e CAMPOS, M. C. M. M. Verificação Formalde Sistemas de Segurança Instrumentados. INDUSCON Conferência Interna-cional de Aplicações Industriais, Abril 2006b.
QUIELLE, J. P. e SIFAKIS, J. Specification and verification of concurrent systemsin CESAR. Em ACM International Symposium on Programming, págs. 337–350,1982.
RAUSCH, M. e KROGH, B. Formal Verification of PLC Programs. Em AmericanControl Confernce − ACC, págs. 234–238, Philadelphia, Pennsylvania, Junho 1998.
SMET, O. e ROSSI, O. Verification of a controller for a flexible manufacturingline written in Ladder Diagram via model-checking. Em American ControlConfernce − ACC, págs. 8–10, Anchorage, Maio 2002.
95
SONG, M. J., KOO, S. R. e SEONG, P. H. Development of a Verification Methodfor Timed Function Blocks Using ESDT and SMV. IEEE International Sym-posium on High Assurance Systems Engineering (HASE’2004), 373(1):285–286, Abril2004.
SPARACO, P. Board Faults Ariane 5 Software. Aviation Week & Space Technology,págs. 33–35, Julho 1996.
VÖLKER, N. e KRÄMER, B. J. Modular Verification of Function Block Basedindutrial Control Systems. Em IFAC-IFIP, págs. 66–71, Schlo Dagstuhl, Germany,Junho 1999.
XIYING, W. e LITZ, L. Model Checking: Towards Generating a Correct Specifi-cation for Logic Contollers. Em American Control Conference - ACC, págs. 8–10,Anchorage, AK, Maio 2002.
96
8 APÊNDICE
97
8.1 MANUAL DO VERIFICADOR DE MODELOS SIMBÓLICOS (SYMBOLIC
MODEL CHECKING - SMV) VERSÃO 2.5.4
Este documento apresenta um resumo do manual da ferramenta SMV, disponível em
CMU (2000).
O SMV é uma ferramenta para verificar sistemas de estados finitos contra especifi-
cações escritas na lógica temporal CTL.
Este documento descreve a sintaxe e a semântica da linguagem de entrada do SMV, e
as funcionalidades do verificador de modelos. Todos os exemplos neste documento estão
disponíveis na distribuição com o software (CMU, 2000).
8.2 LINGUAGEM DE ENTRADA
Considere o programa na linguagem de entra do SMV ilustrado na Figura 8.1 (arquivo
short.smv na distribuição).
1 MODULE main
2 VAR
3 request : boolean;
4 state : {ready,busy};
5 ASSIGN
6 init(state) := ready;
7 next(state) := case
8 state = ready & request : busy;
9 1 : {ready,busy};
10 esac;
11 SPEC
12 AG(request -> AF state = busy)
FIG. 8.1: Listagem de short.smv.
O arquivo de entrada descreve ambos o modelo e a especificação. O modelo é uma
estrutura Kripke, cujo estado é definido por uma coleção de variáveis de estado, que
podem ser booleanas ou escalares. A variável request (pedido) é declarada para ser
booleana na Figura 8.1, enquanto a variável state (estado) é um escalar que assume os
valores ready (disponível) ou busy (ocupado).
A relação de transição da estrutura Kripke, e seu estado inicial (ou estados), são
determinados por uma coleção de atribuições paralelas, que são introduzidas pela palavra
ASSIGN. Na Figura 8.1, o valor inicial da variável state é ready. O valor seguinte de
state é determinado pela expressão na Figura 8.2
O valor de uma expressão case é dado pela primeira expressão no lado direito de um :
98
1 case
2 state = ready & request : busy;
3 1 : {ready,busy};
4 esac;
FIG. 8.2: Expressão
cuja condição no lado esquerdo seja verdadeira. Assim, se state = ready&request for ver-
dadeiro, então o resultado da expressão case é ready, senão, é o conjunto {ready,busy}.
Quando um conjunto é atribuído a uma variável, o resultado é uma escolha não determin-
ista entre os valores disponíveis. Assim, se o valor do state não for ready, ou request
for falso, o valor de state no estado seguinte pode ser ready ou busy. As escolhas não
deterministas são úteis para descrever os sistemas que não estejam ainda inteiramente
implementados, ou para modelos abstratos de protocolos complexos, onde o valor de
algumas variáveis de estado não pode ser determinado completamente.
Observe que request não está atribuído neste programa. Isto deixa o sistema do
SMV livre para escolher qualquer valor para esta variável, dando-lhe a característica de
uma entrada sem restrições para o sistema.
A especificação do sistema aparece como uma fórmula CTL após a palavra-chave
SPEC. O verificador de modelos SMV verifica se todos os possíveis estados iniciais sat-
isfazem à especificação. Na Figura 8.1, a especificação afirma que invariavelmente se
request for verdade, então inevitavelmente o valor de state é busy.
A Figura 8.3 ilustra a definição dos módulos reusáveis e expressões. É um modelo
de circuito contador binário de 3 bits. Observe que o módulo de nome main possui o
significado especial no SMV, na mesma maneira que faz na linguagem de programação
C. A ordem de definições no arquivo de entrada não possui especificação de seqüencia.
Neste exemplo, uma variável pode também ser uma instância de um módulo definido
pelo usuário. O módulo neste caso é o counter_cell, que é instanciado três vezes,
com os nomes bit0, bit1 e bit2. O módulo-célula do contador possui um parâmetro
formal carry_in. Na instância bit0, este parâmetro possui valor 1. Na instância bit1,
carry_in é dado pelo valor de bit0. carry_out. Esta expressão é avaliada no contexto
do módulo principal. Entretanto, uma expressão na forma a.b denota b componente do
módulo a, justo como se o módulo a fosse uma estrutura de dados em uma linguagem de
programação padrão. Daí, carry_in dentro do módulo bit1 é o carry_out do módulo
bit0. A palavra-chave DEFINE é usada para atribuir a expressão value & carry_in para
o símbolo carry_out.
O efeito da indicação DEFINE poderia ter sido obtido declarando uma variável e
99
1 MODULE main
2 VAR
3 bit0 : counter_cell (1);
4 bit1 : counter_cell (bit0.carry_out);
5 bit2 : counter_cell (bit1.carry_out);
6 SPEC
7 AG AF bit2.carry_out
8
9 MODULE counter_cell (carry_in)
10 VAR
11 value : boolean;
12 ASSIGN
13 init (value) := 0;
14 next (value) := value + carry_in mod 2;
15 DEFINE
16 carry_out := value & carry_in;
FIG. 8.3: Programa e expressões reusáveis
atribuindo seu valor, como segue:
1 VAR
2 carry_out : boolean;
3 ASSIGN
4 carry_out := value & carry_in
FIG. 8.4: Atribuição
Observe que neste caso, o valor atual da variável é atribuído, ao invés do valor
seguinte. Os símbolos definidos são às vezes preferíveis às variáveis, desde que não in-
troduzam uma variável nova na representação BDD do sistema. Um ponto fraco dos
símbolos definidos é que não podem ser dados valores não deterministas.
8.3 SINTAXE E SEMÂNTICA
Esta seção descreve a sintaxe e a semântica da linguagem de entrada do SMV.
8.3.1 CONVENÇÕES LÉXICAS
Um átomo na sintaxe descrita abaixo pode ser toda a seqüência dos caracteres no
conjunto {A-Z, a-z, 0-9,_,-}, desde que começem com um caracter alfabético. Todos
os caracteres em um nome são significantes, e maiúsculas e minúsculas são diferenciadas.
Os caracteres de espaço em branco são o espaço, a tabulação e a nova linha. Toda a série
que começa com dois traços (--) e que termina com uma nova linha é um comentário. Um
number é toda a seqüência de dígitos. Todos os outros símbolos analisados e reconhecidos
são incluídos nas citações e expressões da sintaxe abaixo.
100
8.3.2 EXPRESSÕES
As expressões são construídas a partir das variáveis, constantes, e uma coleção de
operadores, inclusive conectivos booleanos, operadores aritméticos inteiros, e expressões
case. A sintaxe das expressões é como segue:
expr ::
atom ;; constante simbólica
| number ;; constante numérica
| id ;; identificador variável
| "!" expr ;; lógica não
| expr1 "&" expr2 ;; lógica e
| expr1 "|" expr2 ;; lógica ou
| expr1 "->" expr2 ;; implicação lógica
| expr1 "<->" expr2 ;; equivalência lógica
| expr1 "=" expr2 ;; igualdade
| expr1 "!=" expr2 ;; desigualdade
| expr1 "<" expr2 ;; menor que
| expr1 ">" expr2 ;; maior que
| expr1 "<=" expr2 ;; menor ou igual que
| expr1 ">=" expr2 ;; maior ou igual que
| expr1 "+" expr2 ;; adição de inteiro
| expr1 "-" expr2 ;; subtração de inteiro
| expr1 "*" expr2 ;; multiplicação de inteiro
| expr1 "/" expr2 ;; divisão de inteiro
| expr1 "mod" expr2 ;; resto de inteiro
| "next" "(" id ")" expr2 ;; valor seguinte
| set_expr ;; uma expressão set
| case_expr ;; uma expressão de case
Uma id, ou identificador, é um símbolo ou expressão que identifica um objeto, tal
como uma variável ou um símbolo definido. Uma vez que uma id pode ser um átomo,
há uma possível ambigüidade se uma variável ou um símbolo definido tiverem o mesmo
nome que uma constante simbólica. Tal ambigüidade é marcada pelo interpretador como
um erro. A expressão next(x) refere-se ao valor do identificador x no próximo estado.
A ordem para analisar a precedência gramatical é, de cima para abaixo,
101
*,/
+,-
mod
=,!+,<,>,<=,>=
!
&
|
->,<->
Operadores de igual precedência se associam à esquerda, como exceção da implicação
->, que se associa à direita. Parênteses podem ser usados para agrupar expressões.
Uma expressão case possui a sintaxe:
case_expr ::
"case"
expr_a1 ":" expr_b1 ";"
expr_a2 ":" expr_b2 ";"
...
expr_an ":" expr_bn ";"
esac
Uma expressão case retorna ao valor da primeira expressão no lado direito, tal que
a condição correspondente no lado esquerdo seja verdadeira. Assim, se expr_a1 for
verdadeiro, então o resultado é expr_b1. Senão, se expr_a2 for verdadeiro, então o
resultado é expr_b2 etc. Se nenhuma das expressões no lado esquerdo for verdadeira, o
resultado da expressão case é o valor numérico 1. É um erro para toda a expressão da
esquerda para retornar um valor diferente de 0 ou 1.
Uma expressão set possui a sintaxe:
dec1 :: "VAR"
atom1 ":" type1 ";"
atom2 ":" type2 ";"
...
O tipo associado a uma declaração variável pode ser um booleano, um escalar, um
módulo definido pelo usuário, ou um vetor de qualquer um dos anteriores.
102
8.3.3 DECLARAÇÃO DA ASSIGN
Uma declaração de atribuição tem a forma:
dec1 :: "ASSIGN"
dest1 ":=" expr1 ";"
dest2 ":=" expr2 ";"
...
onde dest1 e dest2 tem a forma:
dest :: atom
| "init" "(" atom ")"
| "next" "(" atom ")"
No lado esquerdo da atribuição, o átomo denota o valor atual de uma variável,
init(atom) denota seu valor inicial, e next(atom) denota seu valor no próximo estado.
Para que o programa seja implementável, deve ser estabelecido uma ordem em que
as atribuições podem ser executadas tais que nenhuma variável seja atribuída depois que
seu valor seja referenciado. Este não é o caso se houver uma dependência circular entre
as atribuições em qualquer processo dado. Assim, tal circunstância é um erro. Além do
mais, é um erro se a uma variável for atribuído um valor mais de uma vez em em um
dado instante. É um erro se:
a) o valor seguinte ou atual de uma variável for atribuído mais de uma vez em um
processo dado, ou
b) o valor inicial de uma variável for atribuído mais de uma vez no programa, ou
c) o valor corrente e valor inicial de uma variável forem ambos atribuídos no programa,
ou
d) o valor corrente e o valor seguinte de uma variável forem ambos atribuídos no
programa.
8.3.4 DECLARAÇÃO SPEC
A especificação de sistema é dada como uma fórmula na lógica temporal CTL, intro-
duzida pela palavra chave SPEC. A sintaxe desta declaração é:
103
dec1 :: "SPEC" ctlform
Uma formula CTL tem a sintaxe
ctlform ::
expr ;; uma expressão booleana
| "!" ctlform ;; não lógico
| ctlform1 "&" ctlform2 ;; e lógico
| ctlform1 "|" ctlform2 ;; ou lógico
| ctlform1 "->" ctlform2 ;; implicação lógica
| ctlform1 "<->" ctlform2 ;; equivalência lógico
| "E" pathform ;; quantificador de caminho existencial
| "A" pathform ;; quantificador de caminho universal
A sintaxe da fórmula de caminho é:
pathform ::
"X" ctlform ;; próxima vez
"F" ctlform ;; eventualmente
"G" ctlform ;; globalmente
ctlform1 "U" ctlform2 ;; até que
A ordem de precedência dos operadores é (de cima para baixo)
E,A,X,F,G,U
!
&
|
->,<->
Os operadores de precedência igual se associam à esquerda, à exceção da implicação
->, que se associa à direita. Parênteses podem ser usados para agrupar expressões. É
um erro uma expressão em uma fórmula CTL conter um operador next( ) ou retornar
um valor diferente de 0 ou 1. Se houver mais de uma declaração SPEC a especificação é a
conjunção de todas as declarações SPEC. Entretanto, cada uma das fórmulas SPEC é avali-
ada e os resultados são relatados separadamente, um por um, na ordem das declarações
SPEC no texto do programa.
104
8.3.5 DECLARAÇÃO DEFINE
A fim de fazer descrições mais concisas, um símbolo pode ser associado uma expressão
geralmente usada. A sintaxe para esta declaração é:
dec1 :: "DEFINE"
atom1 ":=" expr1 ";"
atom2 ":=" expr2 ";"
...
atomn ":=" expr3 ";"
Quando o identificador que refere-se ao símbolo no lado esquerdo ocorre em uma
expressão, está substituído pela expressão no lado direito. A expressão no lado direito é
avaliada sempre em seu contexto original. As referências prévias para símbolos definidos
são permitidas, mas definições circulares não são, e o resultado é um erro.
8.3.6 MÓDULOS
Um módulo é uma coleção encapsulada de declarações. Uma vez definido, um mó-
dulo pode ser utilizado tantas vezes quanto necessário. Os módulos podem também ser
parametrizados, de modo que cada instância de módulo possa referenciar a diferentes
valores dados. Um módulo pode conter instâncias de outros módulos permitindo que
uma hierarquia estrutural seja construída. A sintaxe de um módulo é a seguinte:
module ::
"MODULE" atom [ "(" atom1 "," atom "," ... atom ")" ]
decl1
decl2
...
decl3
O átomo imediatamente seguido da palavra-chave MODULE é o nome associado ao
módulo. Os nomes de módulo são extraídos de um espaço de nomes distintos dos outros
nomes do programa, e daí podem haver um conflitos entre os nomes das variáveis e das
definições. A lista opcional dos átomos nos parênteses são os parâmetros formais do
módulo. Sempre que estes parâmetros ocorrem nas expressões dentro do módulo, são
substituídos pelos parâmetros reais que são fornecidos quando o módulo é instanciado.
105
Uma instância de módulo é criada usando a declaração VAR. Esta declaração fornece
um nome para a instância, e também uma lista de parâmetros reais, que são atribuídos
aos parâmetros formais na definição do módulo. Um parâmetro real pode ser qualquer
expressão legal. É um erro ser o número de parâmetros reais estiver diferente do número
de parâmetros formais. Por exemplo, na seguinte parte do programa:
...
VAR
a : boolean;
b : foo(a)
...
MODULE foo(x)
ASSIGN
x := 1;
à variável b é atribuída o valor 1. Isto distingüe o mecanismo de chamada por referência
de um esquema de chamada por valor. Considere agora o seguinte programa:
...
DEFINE
a := 0;
VAR
b : bar(a);
...
MODULE bar(x)
DEFINE
a := 1;
y := x;
No programa acima, o valor de y é 0. Por outro lado, usando um mecanismo de chamada
por nome (call-by-name), o valor de y seria 1, desde que a fosse substituído por uma
expressão para x.
Referências prévias para os nomes dos módulos são permitidos, mas as referências
circulares não o são, e o resultado é um erro.
106
8.3.7 IDENTIFICADORES
Um id, ou identificador, é uma expressão que referencia a um objeto. Os objetos são
instâncias dos módulos, variáveis, e símbolos definidos. A sintaxe de um identificador é
a seguinte:
id ::
atom
| id "." atom
| id "[" expr "]"
Um átomo identifica o objeto com esse nome como definido em uma declaração VAR
ou DEFINE. Se a identificar uma instância de um módulo, então a expressão a.b identifica
o objeto componente nomeado b da instância a. Isto é precisamente análogo a acessar
um componente de um tipo estruturado dado. Note que um parâmetro real da instância
de módulo a pode identificar uma outra instância de módulo b, permitindo que a acesse
aos componentes de b, como no exemplo seguinte:
...
VAR
a: foo(b);
b : bar(a);
...
MODULE foo(x)
DEFINE
c := x.p | x.q;
MODULE bar(x)
VAR
p : boolean;
q : boolean;
Aqui, o valor de c é o ou lógico de p e q.
Se a identifica um vetor, a expressão a[b] identifica o elemento b do vetor a. É um
erro para a expressão b avaliar um número fora dos limites subscritos do vetor a, ou um
valor simbólico.
107
8.3.8 MÓDULO MAIN
A sintaxe de um programa de SMV é
program ::
module1
module2
...
modulen
Deve sempre haver um módulo com nome main com nenhum parâmetro formal. O
módulo main é o ponto de partida para avaliação por parte do interpretador.
108
