4.1. TARIM
4.1.3. Başlıca Tarım Ürünleri ve Ekiliş Sahaları
A arquitetura deCRefine foi definida utilizando o padrão MVC e apresenta um bom material que documenta a estratégia utilizada para a sua implementação. Com isso, não tivemos muita dificuldade para entender o funcionamento interno do sistema e, assim, realizar uma extensão na ferramenta.
Para o desenvolvimento do módulo responsável por criar e aplicar as táticas de re- finamento, novos componentes foram inseridos nas camadas já existentes, utilizando os mesmos conceitos das responsabilidades que foram definidas na arquitetura inicial de
CRefine[35].
A Figura 4.7 apresenta uma extensão do diagrama de caso de uso da Seção 4.1. Este novo diagrama ilustra os principais procedimentos que são realizados pelo sistema quando o usuário solicita as novas funcionalidades. Com isso, adicionamos neste diagrama novos casos de uso (ilustrados na cor marrom) a fim de permitir uma visão geral do comporta- mento interno do sistema. O usuário tem a capacidade de executar os seguintes serviços: criar, salvar, abrir, editar, remover, gerar e escolher táticas de refinamento e utilizar o teclado virtual. A opção de gerar uma tática de refinamento realiza o processo de verifi- cação e validação da tática através do parser deArcAngelC, que é realizado pelo sistema. Caso o usuário utilize o teclado virtual, o sistema é responsável por atualizar o editor de táticas com base nos símbolosCircusou macrosArcAngelC selecionados pelo usuário.
Quando o usuário escolhe uma tática para ser aplicada, o sistema realiza sua aplicação de forma automática. Algumas vezes, a aplicação da tática requer a prova de OPs, que
CAPÍTULO 4. ESTENDENDO CREFINE 43
Figura 4.7: Diagrama de Casos de Uso
também é executada pelo sistema. Estas OPs são aquelas relacionadas às leis de refina- mento que fazem parte da tática. Após a aplicação da tática, o sistema atualiza a GUI do
CRefinepara mostrar o resultado dessa aplicação para o usuário.
Para o desenvolvimento do módulo responsável por criar e aplicar as táticas de refina- mento noCRefine, não foi necessário interagir com nenhum framework externo. Entre- tanto, diversas alterações foram realizadas nas camadas existentes. Na camada de apre- sentação adicionamos novas classes dentro do pacote GUI para fornecer a interface desta extensão (como apresentada na seção anterior).
Na camada de dados, foi desenvolvido o módulo Tactics, que é responsável pela cri- ação e aplicação das táticas de refinamento. Neste módulo, foi adicionado o parser de táticas, que segue a sintaxe da linguagemArcAngelC (apresentada na Seção 3). O pacote Applyfornece o suporte para a aplicação das táticas. Ambos os pacotes se comunicam diretamente com o IM, que é a principal classe da camada de gerenciamento responsável por controlar internamente a aplicação. Com isso, o módulo Tactics, através do IM, tem acesso a todos os outros pacotes da ferramenta para realizar o gerenciamento na criação e aplicação das táticas de refinamento. O novo diagrama de classes deCRefine pode ser visualizado na Figura 4.8. Neste diagrama podemos verificar (representado na cor cinza) o novo módulo adicionado que se comunica diretamente com o IM.
CAPÍTULO 4. ESTENDENDO CREFINE 44
Figura 4.8: Diagrama de Classes da Extensão
4.3.1
Criação da Tática
Essa nova extensão possibilita que o usuário possa criar suas próprias táticas de refina- mento e utilizá-las como uma simples regra de transformação. O diagrama de sequência deste processo pode ser verificado na Figura 4.9. A seguir, apresentamos as etapas que fazem parte desse processo:
1. O usuário solicita a opção New Tactic. Essa solicitação é passada para a GUI, que encaminha para o EM;
2. O EM recebe a requisição e inicializa o editor de táticas;
3. Através do editor de táticas, o usuário informa o código ArcAngelC da tática e solicita a opção Generate Tactic. Com isso, a String que contém a especificação da tática de refinamento é enviada para o EM, que insere essa String em um arquivo para realizar o parsing;
4. O EM insere a String em um arquivo e o envia para o IM; 5. O IM recebe o arquivo e o envia para o módulo de táticas;
6. O módulo de táticas recebe o arquivo e encaminha para o pacote Parser, que re- aliza a verificação e validação da tática. Esse processo de compilação envolve a verificação da existência das leis de refinamento utilizadas na tática. Para fazer uso de uma lei de refinamento na tática, é necessário que a lei exista na ferramenta.
CAPÍTULO 4. ESTENDENDO CREFINE 45 Atualmente,CRefinepossui 132 leis de refinamento. A compilação da tática ainda realiza a validação da declaração da tática e de seus argumentos. Uma tática pode receber como argumento: uma lei ou uma tática de refinamento, listas e funções. Entretanto, neste trabalho apenas foram implementadas as funções que fazem parte do estudo de caso, que são: hd (Seção 5.4.1), tl (Seção 5.4.1), join blocks (Se- ção 5.4.2), join all(Seção 5.4.2), join names (Seção 5.4.2), join names 1 (Seção 5.4.2).
7. Se a compilação for bem-sucedida, o sistema armazena o objeto serializado da tática na lista de táticas e envia uma mensagem de sucesso para a GUI. Caso contrário, uma mensagem de erro é apresentada para o usuário.
Figura 4.9: Diagrama de Sequência para Criar uma Tática
4.3.2
Aplicação da Tática
Uma das principais motivações para o desenvolvimento desse módulo na ferramenta
CRefine foi possibilitar um suporte ferramental para a aplicação das táticas de refina- mento no processo do cálculo de refinamentos de programas Circus. O diagrama de
sequência 4.10 ilustra esse processo. As etapas presentes neste diagrama são:
1. O usuário deve selecionar as linhas que podem representar uma ação, um processo ou um programaCircus;
2. O EM disponibiliza um menu pop-up. Através desse menu, o sistema oferece a opção Apply Tactic;
CAPÍTULO 4. ESTENDENDO CREFINE 46
Figura 4.10: Diagrama de Sequência para Aplicar uma Tática 3. O EM envia a solicitação para o IM;
4. O IM consulta o módulo Tactic para pegar a lista que contém todas as táticas de refinamento inseridas na ferramenta que podem ser aplicadas ao termo. Esta lista é formada por objetos serializados do tipo Tactic e é atualizada toda vez que uma tática de refinamento é gerada na ferramenta. Nesta extensão, implementamos a funcionalidade de Filtragem das Táticas de forma parcial, verificando apenas se o primeiro nível da tática de refinamento é aplicado ao termo selecionado. Para a Filtragem das Leis, o CRefine verifica e armazena em uma lista quais leis são aplicáveis ao termo selecionado. Após essa verificação, apenas as leis presentes na lista são disponibilizadas para o usuário. Para tornar possível a Filtragem das Táticas de forma completa é necessário verificar se a tática é aplicável ao termo. Esta verificação só é possível realizando a aplicação da tática ao termo. Entretanto, como uma tática pode englobar inúmeras leis e táticas de refinamento, seria inviável toda vez que a opção Apply Tactic for selecionada realizar a aplicação de todas as táticas ao termo. Por este motivo, apenas realizamos uma verificação parcial; 5. O IM recebe a lista das táticas e envia para o EM;
6. A GUI recebe a lista do EM e disponibiliza para o usuário; 7. O usuário deve selecionar a tática a ser aplicada;
8. O EM recebe o programa selecionado e o insere em uma estrutura (chamada célula de refinamento) que possui dois argumentos: o termo selecionado e as obrigações de prova geradas pela aplicação da tática ao termo.
CAPÍTULO 4. ESTENDENDO CREFINE 47 9. O EM repassa a tática selecionada e a célula de refinamento para o IM;
10. O IM se comunica com o pacote Apply, que fornece o suporte para a aplicação das táticas. Neste pacote, cada construtor deArcAngelCfoi transformado em uma classe Java que herda, em alguns casos de forma indireta, de TacticComponent, uma classe abstrata que possui o método apply. A maioria destas classes implementam esse método de acordo com a semântica de ArcAngelC [37]. Entretanto, a única exceção são as táticas recursivas, cuja implementação é apresentada na Seção 4.3.2; 11. Quando o pacote Apply recebe a requisição do IM, o método apply é invocado utilizando a célula de refinamento como argumento. Todas as implementações do método apply das classes correspondentes aos construtoresArcAngelCde padrões, ações, processos, ações e processos, e de programa verificam se o termo seleci- onado se encaixa na estrutura esperada pela tática. Por exemplo, a classe Java, TSemibox, que corresponde a tática t1 ; t2, verifica se o termo é uma composição sequencial de ações ou processosCircus. Se essa verificação for verdadeira, a tática
t1 é aplicada ao lado esquerdo da composição sequencial e a tática t2 aplicada ao lado direito. Entretanto, caso o termo selecionado inicialmente não seja uma com- posição sequencial, a aplicação da tática falha e uma mensagem de erro é informada para o usuário. A aplicação de uma tática de refinamento pode englobar inúmeras outras aplicações de táticas. Por este motivo, caso essa verificação realizada pelo método apply falhe em algum momento durante a aplicação da tática, então toda a tática falha;
12. Após a aplicação da tática, o pacote Apply retorna para o IM a célula de refinamento atualizada. Esta estrutura agora possui o termo resultante da aplicação da tática e as OPs que foram geradas. Para realizar o descarte das OPs, primeiro a feramenta realiza a prova automática de restrições e funções sintáticas de Z e de Circus para predicados. Caso esta prova automática não ocorra,CRefineinterage com o módulo ZB2SMT. Este módulo tentar provar OPs que sejam predicado. Nesta versão, o módulo ZB2SMT interage com o veriT [6].
13. O IM envia o resultado da aplicação da tática para o EM;
14. O EM gerencia o processo de atualização das janelas da ferramenta; 15. O usuário verifica o resultado da aplicação.
A Figura 4.11 apresenta o diagrama de classes do pacote Apply. Neste diagrama temos a representação da hierarquia das táticas de refinamento da seguinte maneira:
• Táticas básicas (classes na cor azul), que herdam diretamente de TacticComponent; • Táticas unárias (classes na cor marrom), que são formadas por apenas uma tática;
CAPÍTULO 4. ESTENDENDO CREFINE 48 • Táticas binárias (classes na cor verde), que são compostas por duas táticas;
• Táticas n-árias (classe na cor amarela), que possuem um conjunto de táticas.
Figura 4.11: Diagrama de Classes do Pacote Apply
Implementação das Táticas Recursivas
Uma recursão é definida como o menor limite superior de cadeias de aproximação [37] (teorema de Kleenes). A implementação direta da recursão pode gerar um cálculo sem finalização, pois o conjunto das cadeias são potencialmente infinitas.
Para otimizar estas táticas, implementamos duas alternativas para as táticas recursivas: µA e µF. A primeira tática recursiva impõe um limite máximo de aplicações que devem ser executadas. A tática µA verifica o número de iterações realizadas e se comporta como a tática abort, caso a quantidade limite n seja atingida. Esta tática permite utilizar de forma mais segura táticas que podem não terminar. Isto é útil quando não é evidente se, e sob certas condições, as táticas têm a garantia de finalizar. Para estes casos, escolhendo um valor consideravelmente alto para n, podemos obter uma aproximação razoável do comportamento da tática recursiva.
A segunda opção para as táticas recursivas, µF, executa as chamadas recursivas até o número máximo n de iterações. Com isso, quando n é encontrado a tática se comporta
CAPÍTULO 4. ESTENDENDO CREFINE 49 como a tática básica fail.
4.4
Considerações Finais
Este capítulo apresentou o novo módulo desenvolvimento emCRefinepara automati- zar o processo de criação e aplicação das táticas de refinamento. Além disso, detalhamos os novos elementos da interface gráfica, as novas funcionalidades e os componentes arqui- teturais implementados. Na interface gráfica deCRefineadicionamos o itemArcAngelC no menu principal. Este item possibilita ao usuário realizar as funções de criar, abrir, editar e remover uma tática de refinamento. Através deste item, é inicializado o editor de táticas, o qual possibilita definir as táticas de refinamento em ArcAngelC utilizando comandos em LATEX. Para auxiliar o processo de criação e edição de uma tática desenvol-
vemos um teclado virtual que disponibiliza comandosCircuse macros deArcAngelC. Por
fim, a aplicação de uma tática de refinamento utiliza a mesma abordagem para a aplicação de uma lei.
Neste capítulo também descrevemos a nova arquitetura e como ocorre a comunicação do novo módulo com os outros componentes da ferramenta. Para permitir o acesso a todos os pacotes do sistemas, adicionamos este novo módulo na camada de dados e o interagimos diretamente com a classe IM. Com isso, reutilizamos e adaptamos inúmeros métodos para processo de definição e aplicação das táticas de refinamento. Por exemplo, a manipulação e impressão da AST, o processo de aplicação de uma lei e o gerenciamento das OPs.
Nesta extensão implementamos de forma parcial a funcionalidade de Filtragem de Tá- ticas. Esta implementação verifica apenas se o primeiro nível da tática é compatível com o termo que selecionado. Com isso, todas as táticas em que o casamento de padrão no pri- meiro nível for válido são disponibilizadas para o usuário. Como discutido na Seção 4.3 uma implementação completa da Filtragem de Táticas seria inviável, pois seria necessário verificar para todas as táticas de refinamento se a tática é aplicável ao termo.
No novo módulo Tactics implementamos os pacotes Parser e Apply. O primeiro é res- ponsável pelo processo de geração (compilação) de uma tática de refinamento. Neste pa- cote desenvolvemos o parser para a linguagem de táticasArcAngelC. Através deste parser podemos utilizar todos os construtores deArcAngelC para formalizar uma tática de refi- namento. Nesta versão apenas é possível definir táticas através de comandos específicos em LATEX, apresentados no Apêndice F. Entretanto, como trabalho futuro pretendemos
desenvolver comandos em Unicode. O pacote Apply gerencia o processo de aplicação de uma tática de refinamento. Este pacote foi implementado de acordo com a semântica de
CAPÍTULO 4. ESTENDENDO CREFINE 50
ArcAngelC. A única exceção são as táticas recursivas, que possuem duas alternativas: µA e µF.
O desenvolvimento desse novo módulo na ferramenta exigiu a implementação de 115 novas classes e centenas de métodos nas camadas de apresentação e dados. Na camada de gerenciamento nenhuma classe foi desenvolvida. Entretanto, nas classes EM e IM implementamos mais 87 novos métodos para fornecer o suporte para a criação e aplicação das táticas de refinamento, seguindo a arquitetura inicial deCRefine. Além disso, a fim de realizar o estudo de caso que será apresentado no próximo capítulo, foram implementadas na ferramenta mais 26 leis de refinamento e dezenas de obrigações de prova. Por fim, o pacote core.print e o gerador de documentos também foram atualizados. O próximo capítulo descreve o estudo de caso que foi aplicado na ferramenta a fim de validar esse novo módulo emCRefine.
Capítulo 5
Estudo de Caso
Este capítulo apresenta um estudo de caso com o intuito de validar o novo módulo que foi desenvolvido no CRefine. Este módulo é responsável pela criação e aplicação das táticas de refinamento. O estudo de caso consiste em uma estratégia de refinamento que é utilizada na verificação de programa SPARK Ada com relação aos diagramas Si- mulinkcorrespondentes. Na seção 5.1, apresentamos a motivação para a utilização deste estudo de caso. Em seguida, a seção 5.2 informa a estratégia de refinamento utilizada para verificar a implementação dos diagramas Simulink. Na seção 5.3 é fornecida uma breve descrição da especificação abstrata que será refinada. A utilização das táticas de refinamento na estratégia de refinamento é apresentada na seção 5.4. Na seção 5.5, de- monstraremos a aplicação do estudo de caso na ferramenta. Por fim, a seção 5.6 realiza uma avaliação do estudo de caso.
5.1
Contextualização
A verificação e validação de aplicações críticas tem sido uma área de grande interesse [37] pois falhas nestas aplicações podem resultar em prejuízos materiais e humanos. Um exemplo destas aplicações críticas de segurança são os sistemas de controle. Uma das no- tações mais utilizadas para a especificação destes sistemas na indústria são os diagramas de bloco de controle [8].
A complexidade encontrada nos diagramas torna inerente a necessidade da utilização de técnicas para a validação desses diagramas e, principalmente, de suas implementações. Diante disto, Cavalcanti et al. [9] definiu uma nova abordagem voltada para realizar a ve- rificação do código gerado em SPARK Ada, o qual utilizou como base a especificação em diagramas de controle. Essa abordagem define uma semântica para ambos os diagramas de controle e o código SPARK Ada emCircus. A proposta da estratégia é provar que o pro-
gramaCircusque corresponde ao programa SPARK Ada é um refinamento do programa
CAPÍTULO 5. ESTUDO DE CASO 52
Circusque corresponde aos diagramas de controle.
Diagramas de controle modelam sistemas como um grafo dirigido de blocos interco- nectados por fios. A ferramenta Simulink é utilizada para a criação e análise dos diagra- mas, e na geração de código [22]. O uso desta ferramenta é bastante difundido nos setores automobilístico e aéreo. Um simples exemplo de uma diagrama Simulink é apresentado na Figura 5.1. Este diagrama contém um controlador PID (Proportional Integral Deriva- tive), um controlador de mecanismo de feedback genérico que tenta corrigir erros gerando como saída uma ação corretiva que pode ajustar o processo.
Figura 5.1: Controlador PID
Os sistemas de controle apresentam um comportamento cíclico. Cavalcanti et al [9] considera modelos de tempo discreto, na qual as entradas e saídas são apresentadas em intervalos fixos. Tais entradas e saídas são representadas pelos círculos que contêm nú- meros, como pode ser observada na Figura 5.1. Este diagrama possui quatro entradas (E,
Kp,Ki, eKd) e uma saída (Y).
Basicamente, um bloco carrega um sinal de entrada e produz a saída de acordo com a função de cada bloco. Simulink possui bibliotecas que possibilitam definir estes blocos. Os seis blocos presentes na Figura 5.1 são: Diff, Int, Sd, Sp, Si e Sum. Estes blocos simbolizam subsistemas, que representam os sistemas de controle. A Figura 5.2 apresenta o subsistema correspondente ao blocoDiff.
CAPÍTULO 5. ESTUDO DE CASO 53 Os blocos podem ter estado. O bloco Unit Delay (ver Figura 5.2) é responsável por armazenar o valor do sinal de entradaIn1e o valor das saídas. A configuração dos blocos pode utilizar qualquer uma das configurações apresentadas na Figura 5.3 . Entretanto, os blocos deste estudo de caso, inicialmente, utilizam a configuração 4.
Figura 5.3: Configurações dos Blocos
Este estudo de caso foi escolhido, portanto, devido aos seguintes fatores: • Sistemas de controle serem utilizados por sistemas críticos;
• Todas as táticas de refinamento já foram formalizadas e documentadas; • É aplicado a casos reais;
• Por ser complexo o bastante para testar a ferramenta em aplicações complexas. No que se segue, apresentaremos a estratégia de refinamento utilizada para a veri- ficação das implementações dos diagramas Simulink. Em seguida, fazemos uma breve apresentação do modeloCircuscorrespondente aos blocos de diagramas.