Universidade Federal do Rio Grande do NorteCentro de Ciências Exatas e da Terra

Departmento de Informática e Matemática AplicadaPrograma de Pós-Graduação em Sistemas e Computação

Mestrado Acadêmico em Sistemas e Computação

Contribuições para o Processo de Verificaçãode Satisfatibilidade Módulo Teoria em Event-B

Paulo Ewerton Gomes Fragoso

Natal-RN

2015

Paulo Ewerton Gomes Fragoso

Contribuições para o Processo de Verificação deSatisfatibilidade Módulo Teoria em Event-B

Dissertação de Mestrado apresentada ao Pro-grama de Pós-Graduação em Sistemas eComputação do Departamento de Informá-tica e Matemática Aplicada da UniversidadeFederal do Rio Grande do Norte como re-quisito parcial para a obtenção do grau deMestre em Sistemas e Computação.

Linha de pesquisa:Linguagens de Programação e Métodos For-mais

Orientador

Prof. Dr. David Boris Paul Déharbe

PPgSC – Programa de Pós-Graduação em Sistemas e ComputaçãoDIMAp – Departamento de Informática e Matemática Aplicada

CCET – Centro de Ciências Exatas e da TerraUFRN – Universidade Federal do Rio Grande do Norte

Natal-RN

2015

Catalogação da Publicação na Fonte. UFRN / SISBI / Biblioteca SetorialCentro de Ciências Exatas e da Terra – CCET.

Fragoso, Paulo Ewerton Gomes.Contribuições para o processo de verificação de satisfatibilidade módulo teoria em

Event-B / Paulo Ewerton Gomes Fragoso. - Natal, 2015.80 f. : il. Orientador: Prof. Dr. David Boris Paul Déharbe. Dissertação (Mestrado) – Universidade Federal do Rio Grande do Norte. Centro de

Ciências Exatas e da Terra. Programa de Pós-Graduação em Sistemas e Computação. 1. Linguagem de programação – Dissertação. 2. Métodos formais – Dissertação. 3.

Event-B – Dissertação. 4. Obrigações de prova – Dissertação. 5. Plataforma Rodin –Dissertação. 6. Verificação formal – Dissertação. I. Déharbe, David Boris Paul. II.Título.

RN/UF/BSE-CCET CDU: 004.43

Agradecimentos

Agradeço a Deus pela minha vida e por tudo que nela existe. Ao Prof. David Déharbe

por todo tempo e atenção despendidos a mim e à orientação deste trabalho. Ao Prof.

Richard Bonichon pela paciência, interesse e colaboração. Aos amigos do ForALL: João

Souza e Márcio Alves pelo apoio nas disciplinas e na pesquisa; Thiago "Jedi" Abreu

pelas conversas sempre muito agradáveis nos intervalos das atividades; e Vítor Alcântara

pelas dicas sobre o código-fonte do plug-in no início da implementação. Aos conterrâneos,

também integrantes do PPgSC: Ingrid Morgane pela amizade; Héldon José, Laudson

Souza e Hugo Barros pela ajuda na minha adaptação à Natal no começo do curso. Aos

amigos do Laboratório de Mestrado: Eliselma Vieira, Juliana Oliveira e Ronildo Pinheiro

pelo companheirismo. A minha família: Edivania Gomes, Paulo Fragoso, Pablo Edypo e

Elizandra Ewelyn pela presença constante. A minhas grandes amigas: Thaysia Fernandes

por sermos um só às vezes; Amanda Nóbrega e Rivana Araújo por serem essas irmãs que

eu pude escolher.

Contribuições para o Processo de Verificação deSatisfatibilidade Módulo Teoria em Event-B

Autor: Paulo Ewerton Gomes Fragoso

Orientador: Prof. Dr. David Boris Paul Déharbe

Resumo

Event-B é um método formal de modelagem e verificação de sistemas de transição discre-

tos. O desenvolvimento com Event-B produz obrigações de prova que devem ser verifica-

das, isto é, ter sua validade verificada para manter a consistência dos modelos produzidos.

Solucionadores de Satisfatibilidade Módulo Teoria são provadores automáticos de teore-

mas usados para verificar a satisfatibilidade de fórmulas lógicas considerando uma teoria

(ou combinação de teorias) subjacente. Solucionadores SMT não apenas lidam com fórmu-

las extensas em lógica de primeira ordem, como também podem gerar modelos e provas,

bem como identificar subconjuntos insatisfatíveis de hipóteses (núcleos insatisfatíveis). O

suporte ferramental para Event-B é provido pela Plataforma Rodin: um IDE extensível,

baseado no framework Eclipse, que combina funcionalidades de modelagem e prova. Um

plug-in SMT para Rodin tem sido desenvolvido com o objetivo de integrar à plataforma

técnicas alternativas e eficientes de verificação. Neste trabalho foi implementada uma série

de complementos ao plug-in para solucionadores SMT em Rodin, a saber, melhorias na

interface do usuário para quando obrigações de prova são reportadas como inválidas pelo

plug-in. Adicionalmente, algumas características do plug-in, tais como suporte à geração

de provas e extração de núcleo insatisfatível, foram modificadas de modo a tornarem-

se compatíveis com o padrão SMT-LIB para solucionadores SMT. Realizaram-se testes

utilizando obrigações de prova aplicáveis para demonstrar as novas funcionalidades. As

contribuições descritas podem, potencialmente, afetar a produtividade de forma positiva.

Palavras-chave: Event-B, Solucionadores SMT, Plataforma Rodin, Obrigações de prova,

Verificação formal.

Contribuitions to the Satisfability Modulo TheoryChecking in Event-B

Author: Paulo Ewerton Gomes Fragoso

Supervisor: Prof. Dr. David Boris Paul Déharbe

Abstract

Event-B is a formal method for modeling and verification of discrete transition systems.

Event-B development yields proof obligations that must be verified (i.e. proved valid) in

order to keep the produced models consistent. Satisfiability Modulo Theory solvers are

automated theorem provers used to verify the satisfiability of logic formulas considering a

background theory (or combination of theories). SMT solvers not only handle large first-

order formulas, but can also generate models and proofs, as well as identify unsatisfiable

subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin

platform: an extensible Eclipse based IDE that combines modeling and proving features.

A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient

verification techniques to the platform. We implemented a series of complements to the

SMT solver plug-in for Rodin, namely improvements to the user interface for when proof

obligations are reported as invalid by the plug-in. Additionally, we modified some of the

plug-in features, such as support for proof generation and unsat-core extraction, to comply

with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof

obligations to demonstrate the new features. The contributions described can potentially

affect productivity in a positive manner.

Keywords : Event-B, SMT solvers, Rodin platform, Proof obligations, Formal verification.

Lista de figuras

1 Estruturas básicas de máquinas e contextos em um modelo Event-B . p. 19

2 Exemplo de contexto em Event-B . . . . . . . . . . . . . . . . . . . . . p. 20

3 Variáveis da máquina door_0 . . . . . . . . . . . . . . . . . . . . . . . p. 21

4 Eventos da máquina door_0: botão de ativação . . . . . . . . . . . . . p. 22

5 Eventos da máquina door_0: status da porta . . . . . . . . . . . . . . . p. 23

6 Relações entre máquinas e contextos . . . . . . . . . . . . . . . . . . . p. 24

7 Refinamento door_1 da máquina door_0 . . . . . . . . . . . . . . . . . p. 25

8 Evento refinado e novo evento na máquina concreta door_1 . . . . . . p. 26

9 Exemplo de árvore de prova . . . . . . . . . . . . . . . . . . . . . . . . p. 29

10 Arquitetura da Plataforma Rodin . . . . . . . . . . . . . . . . . . . . . p. 31

11 Cadeia de ferramentas em Rodin . . . . . . . . . . . . . . . . . . . . . p. 34

12 Perspectiva de modelagem em Rodin . . . . . . . . . . . . . . . . . . . p. 35

13 Perspectiva de prova em Rodin . . . . . . . . . . . . . . . . . . . . . . p. 36

14 Exemplo de script SMT-LIB . . . . . . . . . . . . . . . . . . . . . . . p. 42

15 Visão esquemática do funcionamento do plug-in SMT para Rodin . . . p. 51

16 Tradução de um sequente simples para o formato SMT-LIB . . . . . . p. 52

17 Script SMT-LIB exemplificando tradução com expressões lambda . . . p. 53

18 Script SMT-LIB exemplificando tradução com ppTrans . . . . . . . . . p. 56

19 Aplicação de tática SMT em Rodin . . . . . . . . . . . . . . . . . . . . p. 56

20 Ciclo de uso do plug-in antes e depois da implementação . . . . . . . . p. 60

21 Detalhe do nó pendente na árvore de prova . . . . . . . . . . . . . . . p. 64

22 Detalhe do nó com contra-exemplo após aplicação do solucionador SMT p. 65

23 Detalhe do resultado unknown . . . . . . . . . . . . . . . . . . . . . . . p. 67

Lista de tabelas

1 Gramática da notação matemática utilizada em Event-B (excerto) . . p. 27

2 Exemplos de lógicas em SMT-LIB . . . . . . . . . . . . . . . . . . . . . p. 43

3 Comandos SMT-LIB . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 44

4 Algumas regras de reescrita implementadas por ppTrans . . . . . . . . p. 54

5 Gramática de ppTrans . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 55

6 Resumo das obrigações de prova . . . . . . . . . . . . . . . . . . . . . . p. 64

7 Resumo das características dos solucionadores utilizados . . . . . . . . p. 64

Lista de abreviaturas e siglas

SMT – Satisfatibilidade Módulo Teoria

CASE – Computer-aided Software Engineering

IDE – Integrated Development Environment

PO – Proof Obligation

POM – Proof Obligation Manager

PUI – Proving User Interface

FNC – Forma Normal Conjuntiva

Sumário

1 Introdução p. 13

1.1 Objetivos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 15

1.2 Experimental . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 16

1.3 Organização do trabalho . . . . . . . . . . . . . . . . . . . . . . . . . . p. 17

2 Event-B e a Plataforma Rodin p. 18

2.1 Componentes de um modelo Event-B . . . . . . . . . . . . . . . . . . . p. 19

2.1.1 Contextos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 19

2.1.2 Máquinas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 20

2.1.2.1 Eventos . . . . . . . . . . . . . . . . . . . . . . . . . . p. 21

2.2 Componentização . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 23

2.3 Refinamento . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 24

2.4 Linguagem matemática . . . . . . . . . . . . . . . . . . . . . . . . . . p. 25

2.5 Obrigações de prova . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 26

2.6 Rodin . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 30

2.6.1 Arquitetura . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 31

2.6.1.1 Plataforma Rodin . . . . . . . . . . . . . . . . . . . . p. 32

2.6.1.2 Pacotes da biblioteca Event-B . . . . . . . . . . . . . . p. 32

2.6.1.3 Núcleo Event-B . . . . . . . . . . . . . . . . . . . . . . p. 32

2.6.1.4 Interface do Usuário Event-B . . . . . . . . . . . . . . p. 34

2.7 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 35

3 Solucionadores SMT e o padrão SMT-LIB p. 37

3.1 Solucionadores SMT . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 38

3.2 SMT-LIB . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 40

3.2.1 A linguagem SMT-LIB . . . . . . . . . . . . . . . . . . . . . . . p. 41

3.3 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 44

4 Integração de solucionadores SMT à Plataforma Rodin p. 46

4.1 Motivação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 46

4.2 Histórico . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 48

4.2.1 SMT e Método B . . . . . . . . . . . . . . . . . . . . . . . . . . p. 48

4.2.2 SMT e Event-B . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 49

4.2.3 Retorno para obrigações de prova não descartadas em Rodin . . p. 49

4.3 Funcionamento e características . . . . . . . . . . . . . . . . . . . . . . p. 50

4.3.1 Tradução . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 51

4.3.1.1 Abordagem com expressões lambda . . . . . . . . . . . p. 52

4.3.1.2 Abordagem com ppTrans . . . . . . . . . . . . . . . . p. 53

4.3.2 Verificação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 54

4.3.3 Resposta . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 56

4.4 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 57

5 Implementando retorno para obrigações de prova não-verificadas e

padronização SMT-LIB p. 58

5.1 Metodologia . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 59

5.2 Abordagem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 61

5.3 Resultados e discussão . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 63

6 Considerações finais p. 68

6.1 Principais contribuições . . . . . . . . . . . . . . . . . . . . . . . . . . p. 69

6.2 Limitações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 69

6.3 Trabalhos futuros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 70

Referências p. 71

13

1 Introdução

Métodos formais consistem no desenvolvimento e aplicação de técnicas matemáticas na

construção de sistemas, incluindo software e hardware. A ideia é que o uso de metodologias

mais rigorosas contribui para a criação de sistemas mais confiáveis, do ponto de vista da

fidedignidade em relação aos requisitos, bem como das restrições de qualidade e segurança.

Praticamente todas as etapas do ciclo de desenvolvimento de software são passíveis

à aplicação de métodos formais, sendo esta mais comum nas áreas de engenharia de

requisitos, a partir de especificações formais e de verificação − comumente, corretude de

programas e análise de especificação de sistemas por meio de provas (WOODCOCK et al.,

2009).

Especificação consiste na atividade de gerar um documento ou modelo que corres-

ponda a um conjunto de requisitos de determinado sistema. Em métodos formais, uma

especificação é expressa numa linguagem com sintaxe e semântica rigorosamente definidas

(SOMMERVILLE, 2007). As atividades de especificação e verificação formal estão intima-

mente relacionadas: verificam-se os modelos construídos como forma de certificação destes

em relação aos requisitos a que correspondem, por exemplo.

Ainda de acordo com Sommerville (2007), as técnicas de especificação formal de soft-

ware podem ser dividas em dois grandes grupos:

• Abordagem algébrica: baseada no conceito de definição de interfaces entre subsis-

temas e o relacionamento de suas operações; exemplos desse método incluem Larch

(GUTTAG et al., 1993) e Lotos (BOLOGNESI; BRINKSMA, 1987);

• Abordagem baseada em modelos (ou comportamental): utilização de estruturas ma-

temáticas, tais como conjuntos, para representar o sistema; operações são definidas

a partir da forma como modificam o estado do sistema modelado; esta abordagem

é utilizada em formalismos tais como Z (SPIVEY, 1992) e VDM (JONES, 1986).

No campo de verificação formal, é possível citar como principais técnicas (WOODCOCK

14

et al., 2009):

• Verificação de modelos: um modelo finito representando o sistema é criado e verifi-

cado em relação aos requisitos especificados;

• Prova de teoremas: propriedades da especificação do sistema são representadas por

meio de teoremas de uma determinada lógica, que devem ter sua validade verificada;

esta verificação (prova) é geralmente realizada de modo automático por ferramentas

específicas, os provadores.

• Interpretação abstrata: formalização do conceito de aproximação em semânticas de

linguagens de programação, aplicada, principalmente, à análise estática de software.

Event-B (ABRIAL, 2010) é um método formal de desenvolvimento de sistemas que

inclui etapas de especificação baseada em modelos e verificação. Em Event-B, um modelo

de sistema é construído incrementalmente, isto é, a partir de uma representação mais

simples, detalhes vão sendo adicionados, visando obter versões cada vez mais completas.

A tal processo de transformação do modelo de uma versão mais abstrata a uma mais

concreta (refinada) dá-se o nome de refinamento. Este pode ser classificado em dois tipos

básicos: horizontal, que visa a cobertura, no modelo construído, de todos os requisitos

definidos para o sistema; e vertical, no qual se transformam partes da especificação de

modo que possam ser implementadas em uma linguagem de programação.

Provas matemáticas precisam ser realizadas para garantir a consistência entre um

nível de abstração e outro. Isto é possível por meio da verificação de obrigações de prova

(teoremas sobre a especificação) produzidas durante o desenvolvimento.

O suporte automatizado para a aplicação de Event-B é obtido por meio da Plata-

forma Rodin (ABRIAL et al., 2006), uma ferramenta que integra funções de modelagem

e verificação formal. Ela conta com funcionalidades importantes tais como a produção e

prova automática de obrigações de prova, expressas em lógica de primeira ordem. Dife-

rentes tipos de provadores automáticos estão disponíveis para realização do processo de

verificação de obrigações de prova em Rodin.

Este trabalho tem como interesse o aprimoramento de uma dessas ferramentas de ve-

rificação: o plug-in que permite o uso de solucionadores do tipo Satisfatibilidade Módulo

Teoria (SMT) na verificação de obrigações de prova produzidas por Rodin (DÉHARBE,

2010). Solucionadores SMT vêm sendo cada vez mais utilizados no âmbito de métodos

formais, em diferentes tipos de aplicações (BARRETT et al., 2009). Características de solu-

15

cionadores SMT, tais como produção de provas e contra-modelos, além da capacidade de

lidar com fórmulas extensas de lógica de primeira ordem, tornam o uso deste tipo de pro-

vador uma escolha particularmente útil no processo de verificação da classe de obrigações

de prova geradas no desenvolvimento com Event-B.

1.1 Objetivos

O objetivo geral deste trabalho é aprimorar o processo de verificação de obrigações de

prova, na Plataforma Rodin, durante a utilização de seu plug-in SMT. Especificamente,

foi implementado tratamento e feedback ao usuário quando uma obrigação de prova não

é verificada, isto é, quando o retorno do solucionador SMT for sat ou unknown. Estes

resultados indicam, respectivamente, que a fórmula (produzida como uma negação do

sequente original) é inválida ou que não pode ser verificada devido a alguma limitação

do solucionador utilizado. Adicionalmente, foram padronizadas características do plug-in

tais como suporte à produção de provas e extração de núcleo insatisfatível, ao padrão

SMT-LIB.

Como objetivos específicos alcançados durante a pesquisa é possível citar:

• Estudo do código-fonte de ambos Rodin e plug-in SMT: identificação de caracte-

rísticas do projeto, visando a ter uma perpectiva mais sólida em relação à imple-

mentação do componente e de como modificá-lo adequadamente para adicionar as

funcionalidades previstas;

• Avaliação de como o plug-in trata o resultado retornado pelo solucionador SMT:

necessário para identificar de que forma a saída do solucionador pôde ser explorada,

especialmente quando o resultado for sat ou unknown;

• Levantamento das formas com que a interface do usuário pôde ser modificada du-

rante a interação com o plug-in: identificação de modos de gerar retorno útil ao

usuário quando uma obrigação de prova não for verificada;

• Exploração de características do padrão SMT-LIB: análise de comandos que pu-

deram ser usados para extração de núcleos insatisfatíveis e geração de modelos de

prova, por exemplo;

• Comparação das funcionalidades dos solucionadores SMT compatíveis com o plug-

in: avaliação de limitações e compatibilidade com SMT-LIB;

16

• Implementação das contribuições propostas: codificação das novas funcionalidades

referentes à experiência de uso e padronização do plug-in;

• Validação da pesquisa com estudo de caso: realização de testes com solucionadores

SMT compatíveis e obrigações de prova passíveis de utilização.

1.2 Experimental

Uma pesquisa bibliográfica foi realizado no início do trabalho com o objetivo de le-

vantar informações acerca do estado atual do plug-in SMT para a Plataforma Rodin,

bem como elucidar as características das demais tecnologias de interesse, isto é, o método

Event-B e os solucionadores SMT. A fundamentação teórica, presente no decorrer de todo

o texto, é resultado desta fase.

Ao levantamento bibliográfico inicial, se seguiram testes de uso da Plataforma Rodin.

Foi utilizada a versão 3.0.1 com o plug-in SMT Solvers versão 1.2.1 instalado. A ideia era

editar especificações Event-B e realizar o processo de verificação de obrigações de prova

geradas pela ferramenta utilizando diferentes solucionadores SMT. Os projetos Rodin

trabalhados foram escolhidos de forma arbitrária, recuperados do Repositório DEPLOY1.

Esta fase tinha dois objetivos básicos: observar o ponto de vista do usuário, atentando

para as características da interface gráfica, no ciclo de modelagem e prova; e registrar

o comportamento da plataforma no uso da tecnologia de verificação com solucionado-

res SMT. O resultado desta fase consiste na abordagem de implementação utilizada na

exibição dos resultados na interface de Rodin e as comparações de capacidades entre os

diferentes provadores compatíveis com o plug-in.

Paralelamente aos testes com a Plataforma Rodin, foram explorados, no sentido de

terem suas funcionalidades testadas com scripts SMT-LIB, diversos solucionadores SMT.

O objetivo era observar as saídas das ferramentas para os diversos comandos disponíveis

na linguagem de interação, bem como comparar as características de cada provador. Um

apanhado geral das características dos solucionadores testados pode ser conferido na Seção

5.3. Os resultados desta etapa permitiram abordar de forma prática, no código-fonte do

plug-in, os comandos citados na Seção 5.1.

O prosseguimento da pesquisa se deu com o estudo do código-fonte do plug-in. Nesta

etapa, levantou-se uma forma apropriada de implementação das funcionalidades propostas1http://deploy-eprints.ecs.soton.ac.uk/view/type/

17

nos objetivos do trabalho. A codificação foi realizada na IDE Eclipse, versão RCP 4.4.0,

utilizando a linguagem de programação Java 2, em sua versão 6.

Após a implementação, as funcionalidades foram testadas na Plataforma Rodin de

forma a demonstrar os resultados esperados. Informações sobre os projetos utilizados,

resultados obtidos e demais peculiaridades de tal demonstração podem ser consultadas

no Capítulo 5.

1.3 Organização do trabalho

O restante deste trabalho está organizado como segue: o Capítulo 2 contém embasa-

mento sobre o método Event-B e a Plataforma Rodin; o Capítulo 3 informa fundamentos

de solucionadores SMT e do padrão SMT-LIB; no Capítulo 4, discorre-se sobre caracterís-

ticas e funcionamento do plug-in SMT para Rodin; no Capítulo 5 descreve-se o processo

de execução dos objetivos propostos; e no Capítulo 6 apontam-se as considerações finais

do trabalho.

2http://java.oracle.com

18

2 Event-B e a Plataforma Rodin

Event-B (ABRIAL, 2010) é um processo formal de modelagem e análise de sistemas

de transição discretos, considerado uma extensão do método B (ABRIAL, 1996) de desen-

volvimento de programas. Diferenças entre os dois formalismos incluem a separação das

partes estática (contextos) e dinâmica (máquinas) do modelo em Event-B e a mudança

de foco de aplicação: utiliza-se o método B no desenvolvimento de componentes de soft-

ware, ao passo que em Event-B todo o sistema é formalizado. Assim, é possível levar em

consideração durante a modelagem uma aproximação do ambiente em que o sistema está

inserido, bem como outros tipos de componentes tais como hardware.

No contexto de Event-B, um sistema é constituído por um conjunto de estados e

transições sobre estes. Variáveis e constantes denotam o estado, ao passo que eventos

representam as transições. A representação dos modelos é feita a partir de notação ma-

temática, composta de construções diversas incluindo teoria de conjuntos e lógica de

primeira ordem. Isto permite raciocinar formalmente sobre os requisitos especificados de

um sistema por meio de provas.

O suporte ferramental CASE para modelagem com Event-B consiste na Plataforma

Rodin (ABRIAL et al., 2010): uma IDE extensível, isto é, capaz de ter suas funcionalidades

estendidas ou melhoradas por meio de complementos (plug-ins), baseada no framework

Eclipse1. No decorrer deste capítulo, apresentam-se as características fundamentais de

Event-B e Rodin, com o objetivo de facilitar o entendimento do restante do trabalho.

Especificamente, abordam-se a estrutura e características de um modelo em Event-B, a

linguagem matemática utilizada, bem como as ideias de refinamento, componentização

e obrigações de prova. Sobre Rodin, registram-se as características básicas e o uso da

ferramenta no processo de especificação formal e prova.1http://www.eclipse.org

19

2.1 Componentes de um modelo Event-B

Um modelo Event-B é composto por dois tipos de estruturas: contextos e máquinas.

Contextos se referem à parte estática (constantes) do sistema, enquanto máquinas se refe-

rem à parte dinâmica (variáveis). Ambos constituem-se de seções (cláusulas) estruturais.

Os padrões básicos de estrutura são ilustrados na Figura 1. É importante observar que

algumas cláusulas podem estar vazias na definição de máquinas e contextos. Por exemplo,

é possível que determinado contexto seja formado apenas por constantes e axiomas sobres

estas, não sendo necessário definir conjuntos e teoremas.

Os exemplos de máquinas e contextos citados nesta seção são inspirados no estudo de

caso descrito em Déharbe et al. (2007). Nele, descreve-se parte de um modelo simplificado

de sistema controlador de abertura e fechamento de portas de vagões em um trem.

Figura 1: Estruturas básicas de máquinas e contextos em um modelo Event-B

Fonte: Adaptado de Abrial (2010)

2.1.1 Contextos

Um contexto pode conter as seguintes cláusulas:

• SETS: declaração de conjuntos definidos pelo usuário; pode-se declarar apenas os

identificadores de cada conjunto (neste caso, supõe-se apenas que os conjuntos não

são vazios) ou criar enumerações;

• CONSTANTS: listagem das constantes presentes no contexto;

• AXIOMS: os axiomas definem o tipo de cada constante e demais restrições asso-

ciadas;

• THEOREMS: consequências lógicas que devem ser provadas utilizando os axio-

mas definidos e demais teoremas enunciados, inclusive aqueles estendidos de outros

20

contextos (vide Subseção 2.2).

Na Figura 2 é ilustrada a especificação de um contexto Event-B, onde a situação atual

de uma porta é modelada pelo conjunto STATUS, formado pelas contantes open e closed.

O operador partition é uma maneira de representar os axiomas STATUS = {open, closed}e open 6= closed.

CONTEXT door_ctx0SETS

STATUSCONSTANTS

open

closedAXIOMS

axm1 : partition(STATUS, {open}, {closed})END

Figura 2: Exemplo de contexto em Event-B

2.1.2 Máquinas

Uma máquina pode ser constituída das seguintes cláusulas:

• VARIABLES: listagem dos identificadores de variáveis;

• INVARIANTS: declaração dos tipos e restrições associadas às variáveis definidas,

na forma de proposições e predicados; deve-se garantir a validade dos invariantes

durante todo o funcionamento do sistema;

• THEOREMS: teoremas a serem provados; a escrita destes pode facilitar a prova

de determinadas propriedades da máquina;

• VARIANT: o variante é uma expressão avaliada em um número natural ou con-

junto finito que serve para determinar a convergência de eventos, isto é, a prova de

que novos eventos adicionados a uma máquina refinada (vide Subseção 2.3) não irão

executar indefinidamente, impedindo que os eventos abstratos previamente definidos

sejam habilitados;

21

• EVENTS: seção de definição de eventos.

Por exemplo, seja a máquina door_0, parte da especificação do controlador de por-

tas que inclui o contexto da Subseção 2.1.1. São declaradas duas variáveis status e but-

ton_pressed que representam, respectivamente, a situação atual da porta (aberta ou fe-

chada) e o status do botão que ativa manualmente a abertura ou fechamento (Figura

3).

É possível notar que determinadas partes da especificação, tais como invariantes e

axiomas, são rotuladas de modo único em cada máquina ou contexto. Os rótulos inv0_0 e

inv0_1, por exemplo, estão escritos seguindo a convenção de indicar a versão da máquina

(door_0) e atribuir um número sequencial aos invariantes. O objetivo de sistematizar

a atribuição de rótulos é promover a rastreabilidade entre os diferentes elementos que

compõem os artefatos do projeto, incluindo documentos de levantamento de requisitos.

O editor de especificações padrão de Rodin (vide seção 2.6.1.4), Rodin Editor, é capaz de

gerar rótulos automaticamente, de modo padronizado.

MACHINE door_0SEES door_ctx0VARIABLES

status

button_pressedINVARIANTS

inv0_0 : status ∈ STATUSinv0_1 : button_pressed ∈ BOOL

Figura 3: Variáveis da máquina door_0

2.1.2.1 Eventos

Eventos determinam as transições de estado numa máquina. Assim como máquinas e

contextos, os eventos também são estruturados em cláusulas, a saber:

• ANY: identificadores dos parâmetros do evento;

• WHERE: definição dos tipos de cada um dos parâmetros declarados e das guardas

22

(condições); o conjunto de guardas deve ser satisfeito para que um evento seja habi-

litado; em eventos sem parâmetros, a palavra reservada WHEN pode ser utilizada

para identificar a cláusula;

• WITH: testemunhas (witnessess) são declarações que devem fazer referência a pa-

râmetros eliminados em versões refinadas de determinado evento;

• ACTION: definição das ações executadas na ocorrência do evento.

Os eventos press_button e release_button modelam a ativação/desativação manual

do botão por um operador (Figura 4). O cabeçalho da cláusula EVENTS, bem como o

evento de inicialização foram omitidos. Os eventos open_door e close_door representam

abertura e fechamento das portas, respectivamente (Figura 5).

Event press_button =̂when

grd0_1 : button_pressed = FALSEthen

act0_3 : button_pressed := TRUEend

Event release_button =̂when

grd0_2 : button_pressed = TRUEthen

act0_4 : button_pressed := FALSEend

Figura 4: Eventos da máquina door_0: botão de ativação

Ações consistem de atribuições às variáveis da máquina. Existem dois tipos básicos de

atribuições: determinísticas e não-determinísticas. Uma atribuição determinística segue

o formato := . Por exemplo, na máquina door_0, o evento

open_door (Figura 5) possui a seguinte atribuição determinística: status := open. Já na

atribuição não-determinística, tem-se o formato :| . Nestecaso, no lado direito do operador encontra-se um predicado de antes e depois que deve fazer

referência à variável do lado esquerdo. Atribuições determinísticas podem ser normalizadas

ao formato não-determinístico. Por exemplo, a atribuição anterior reescrita de forma não-

determinística é equivalente a status :| status′ = open, onde status′ representa o estado da

23

variável status após a ocorrência da ação. Um caso mais específico deste tipo de atribuição

é :∈ . Por exemplo: status :∈ STATUS;normalizada, torna-se status :| status′ ∈ STATUS.

Event open_door =̂when

grd0_3 : status = closedgrd0_4 : button_pressed = TRUE

then

act0_5 : status := openend

Event close_door =̂when

grd0_5 : status = opengrd0_6 : button_pressed = FALSE

then

act0_5 : status := closedend

Figura 5: Eventos da máquina door_0: status da porta

2.2 Componentização

Um modelo pode ser decomposto em diversas partes menores com o objetivo de ge-

renciar a complexidade. Neste sentido, é possível fazer com que propriedades sejam com-

partilhadas entre cada uma das partes. Utilizam-se as palavras reservadas extends, na

definição de componentização (extensão) entre contextos, e sees para comunicar máqui-

nas e contextos.

Um contexto pode estender um número arbitrário de outros contextos. Isto é, se um

contexto Ctx_1 estende um contexto Ctx_0, então os conjuntos e contantes presentes

em Ctx_0 podem ser usados nas declarações de Ctx_1. Esta característica é transitiva,

ou seja, Ctx_1 também estenderia, indiretamente, as propriedades de outros contextos

estendidos por Ctx_0. Adicionalmente, uma máquina pode ver zero ou mais contextos,

permitindo acesso às propriedades de cada um. Uma esquematização de como se dá a

comunicação entre os diversos componentes de um modelo é ilustrada na Figura 6.

24

Figura 6: Relações entre máquinas e contextos

Fonte: Abrial (2010)

2.3 Refinamento

No início do desenvolvimento, um modelo consiste geralmente de uma versão mais

abstrata e simples do sistema. À medida em que o processo evolui, novos detalhes são

adicionados de forma a garantir a cobertura de todos os requisitos definidos na fase inicial.

Desse modo, diversas versões do modelo vão sendo criadas sucessivamente, cada uma

correspondendo a uma evolução da anterior. Essa ideia de incrementalidade está ligada,

em Event-B, ao conceito de refinamento.

Uma máquina pode refinar uma outra máquina. Esta é então chamada de máquina

abstrata e aquela de máquina concreta. O refinamento é explicitado pela palavra reservada

refines na definição da máquina concreta. É importante destacar que uma máquina refi-

nada não possui acesso direto às propriedades de contextos vistos por sua versão abstrata:

é preciso definir explicitamente todos os contextos necessários.

A máquina concreta pode conter novas variáveis e, consequentemente, novos invarian-

tes. Quando um invariante se refere a uma ou mais variáveis abstratas, tem-se um invari-

ante de ligação. A declaração de um refinamento da máquina door_0 pode ser conferida

na Figura 7. São declaradas três novas variáveis: speed_limit, train_speed e train_stopped.

As duas primeiras referem-se, respectivamente, a um limite pré-determinado de velocidade

relativo ao acionamento do botão de abertura de porta e à velocidade atual do trem. A

terceira é uma variável booleana que indica se o trem está ou não em movimento.

É possível haver também eventos concretos que são refinamentos daqueles na máquina

25

MACHINE door_1REFINES door_0SEES door_ctx0VARIABLES

status

button_pressedspeed_limittrain_speedtrain_stopped

INVARIANTS

inv1_1 : speed_limit ∈ Ninv1_2 : train_speed ∈ Ninv1_3 : train_stopped ∈ BOOL

Figura 7: Refinamento door_1 da máquina door_0

abstrata, bem como se pode definir novos eventos. Estes, na realidade, são também refina-

mentos de suas respectivas versões abstratas sem guardas e com ação skip (sem mudança

de estado). Trata-se de um mecanismo utilizado para garantir a correspondência entre as

máquinas: um evento que existe na máquina concreta também deve existir na máquina

abstrata.

O evento abstrato press_button da máquina door_0 é refinado na máquina door_1,

adicionando-se uma nova guarda: o botão só poderá ser acionado caso o trem esteja parado

ou o limite de velocidade não tenha sido superado. Um novo evento, que permite definir

o limite de velocidade para acionamento do botão de abertura, também é adicionado à

máquina concreta. Ambos os eventos podem ser conferidos na Figura 8.

2.4 Linguagem matemática

Em Event-B, são utilizados na definição de máquinas e contextos, bem como no pro-

cesso de raciocínio (prova) sobre o modelo, basicamente dois tipos de estruturas: expres-

sões e predicados. Expressões representam objetos no modelo (variáveis ou pares ordena-

dos), ao passo que cada predicado pode ser avaliado como verdadeiro ou falso. A notação

matemática para expressar tais construções consiste na combinação de fragmentos de di-

26

Event press_button =̂refines press_button

when

grd1_0 : (train_speed ≤ speed_limit) ∨ (train_stopped = TRUE)grd1_1 : button_pressed = FALSE

then

act1_3 : button_pressed := TRUEend

Event set_speed_limit =̂any

limitwhere

grd1_5 : limit ∈ Nthen

act1_6 : speed_limit := limitend

Figura 8: Evento refinado e novo evento na máquina concreta door_1

versas linguagens, a saber: linguagem proposicional e de predicados, igualdade, teoria dos

conjuntos, valores booleanos e aritmética de inteiros.

Na Tabela 1, a seguir, são ilustradas porções, adaptadas de Abrial (2010), da gramática

da notação matemática passíveis de serem utilizadas durante a especificação. É possível

consultar uma versão condensada da notação matemática de Event-B em Robinson (2010).

2.5 Obrigações de prova

Uma série de propriedades precisa ser provada válida num modelo Event-B com o

objetivo de garantir a consistência de cada uma das etapas no processo de especificação

formal. Particularmente, é necessário provar que, para cada transição ocorrida numa má-

quina, esta não é levada a um estado inválido, isto é, necessita-se provar a preservação

dos invariantes para cada ocorrência de eventos. Outra propriedade importante a ser ve-

rificada é a correspondência entre refinamentos e seus respectivos modelos abstratos. As

provas destas, entre outras características da especificação, são realizadas por meio da

verificação de obrigações de prova geradas durante o desenvolvimento.

27

Tabela 1: Gramática da notação matemática utilizada em Event-B (excerto)Proposições, predicadospredicado ::= ⊥

>¬predicadopredicado ∧ predicadopredicado ∨ predicadopredicado⇒ predicadopredicado⇔ predicado∀var_lista · predicado∃var_lista · predicadoexpressão = expressãoexpressão ∈ expressãoexpressão ⊆ expressão

Conjuntosexpressão ::= ∅

expressão⋃expressão

expressão⋂expressão

expressão \ expressãoexpressão× expressão⋃var_lista · predicado | expressão⋂var_lista · predicado | expressão

P(expressão){var_lista · predicado | expressão}inter(expressão)union(expressão)

Relações, funçõesexpressão ::= expressão 7→ expressão

expressão↔ expressãoexpressão 7→ expressãoexpressão→ expressãodom(expressão)ran(expressão)

Aritmética, booleanosexpressão ::= N

ZBOOLFALSETRUEexpressão+ expressãoexpressão− expressãoexpressão× expressão

28

Uma obrigação de prova (ou PO , proof obligation) consiste de um sequente (GENTZEN,

1935): construção no formato H ` G, onde H e G são meta-variáveis que correspondem,respectivamente, a um conjunto de hipóteses (possivelmente vazio) e a uma conclusão.

Assim, diz-se que G é demonstrável sob H. Hipóteses e conclusão são escritos na forma de

predicados sobre as propriedades do modelo. Por exemplo, seja a PO relativa à preservação

dos invariantes (identificada como INV) que deve ser provada para cada invariante e evento

presente em uma máquina abstrata:

A(s, c)

I(s, c, v)

G(s, c, v, x)

BA(s, c, v, x, v′)INV

inv(s, c, v′)

onde, s e c representam, respectivamente, os conjuntos e contantes definidos nos contextos

vistos direta ou indiretamente pela máquina; v e v′ os estados das variáveis antes e depois

das atribuições ocorridas no evento; x os parâmetros do evento; A os axiomas; I os inva-

riantes; G as guardas do evento; BA os predicados de antes e depois para cada atribuição

de variável no evento; e inv o invariante modificado após a ocorrência do evento.

Por exemplo, a obrigação de prova de preservação do invariante inv1_1 da máquina

door_1 (Figura 7) para o evento set_speed_limit (Figura 8) é dada por:

speed_limit ∈ N

train_speed ∈ N

train_stopped ∈ BOOL

speed_limit′ = limit

limit ∈ N

`

limit ∈ N

A prova de uma PO é formada por uma árvore com restrições, gerada a partir do pro-

cesso de cálculo de sequentes, isto é, transformações sobre estes ao aplicarem-se regras de

inferência (ou de prova). Uma regra de prova segue o formato

AC

onde A constitui os antecedentes e C o consequente da regra. A representa um conjunto

de sequentes (possivelmente vazio) e C um único sequente. Para conseguir uma prova de

29

C, é necessário obter provas de cada um dos sequentes presentes em A. Uma teoria é

formada pelo conjunto de regras de prova utilizadas na prova de uma PO.

As restrições sobre a árvore de prova são as seguintes: cada nó é formado por um

sequente a ser provado e uma regra associada; a raiz contém o sequente original (PO); e

as folhas devem ser axiomas (sequentes sem antecedentes). Ou seja, aplica-se uma regra de

prova sobre a PO, gerando zero ou mais nós com sequentes que correspondem justamente

a cada um dos antecedentes da regra. Novas regras de inferência são aplicadas aos nós

gerados até que existam somente sequentes que não necessitem mais ser transformados.

Um exemplo de árvore de prova é exibido na Figura 9. Nela, é possível notar que a

regra R3 aplicada ao sequente S1 (raiz), produz três novos nós com os sequentes S2, S3

e S4, com suas respectivas regras de inferência R1, R5 e R2. Isto gera a finalização da

prova com os axiomas S2/R1, S5/R4, S6/R6 e S7/R7, em que a aplicação das regras de

prova não gera novos sequentes.

Figura 9: Exemplo de árvore de prova

Fonte: Adaptado de Abrial (2010)

Uma prova simples da PO INV mostrada anteriormente é ilustrada abaixo. Ao lado

30

de cada sequente indica-se a regra de inferência aplicada.

speed_limit ∈ N

train_speed ∈ N

train_stopped ∈ BOOL

speed_limit′ = limit

limit ∈ N limit ∈ N

` MON ` HYP

limit ∈ N limit ∈ N

As duas regras de prova utilizadas acima são:

H1 ` G MONH1, H2 ` G

HYPP ` P

Um apanhado geral dos tipos de obrigações de prova, bem como de regras de inferência

e simplificações a sequentes utilizadas comumente no processo de prova em Event-B, pode

ser consultado em Abrial (2010).

2.6 Rodin

O desenvolvimento da Plataforma Rodin tem sido apoiado, no decorrer dos anos, por

projetos que reúnem parceiros da academia e indústria no incentivo à disseminação de

métodos formais para a criação de sistemas mais confiáveis (EVENT-B, 2014).

Rodin é construída sobre o framework Eclipse, beneficiando-se de características tais

como responsividade da ferramenta em relação a mudanças no modelo, automatização de

verificações estáticas (por exemplo, verificação de tipo) e extensibilidade. A plataforma

foi concebida para suportar, de forma integrada, tanto a atividade de modelagem quanto

de prova (ABRIAL et al., 2006). A ideia é que a transição entre uma tarefa e outra aconteça

de modo mais transparente e intuitivo para o usuário. Um exemplo dessa integração é a

geração de obrigações de prova: os mesmos predicados definidos nos invariantes e guardas

são utilizados nas POs, facilitando o rastreio das hipóteses (por meio de rótulos) junto ao

modelo.

31

2.6.1 Arquitetura

Rodin é composta por conjuntos de componentes interconectados que funcionam em

sincronia, mantendo a responsividade da plataforma em relação ao modelo no que se refere

à verificação estática, geração de POs e provas, a cada modificação realizada pelo usuário.

Por exemplo, Rodin implementa um mecanismo de filtragem automática em três etapas

que possibilita o reaproveitamento de provas já realizadas em obrigações de prova, cujas

partes relevantes não foram modificadas durante uma dada edição do modelo (ABRIAL et

al., 2010).

Na Figura 10, é possível ter uma visão hierárquica da arquitetura da plataforma.

Pode-se observar a separação dos componentes (retângulos sólidos) em conjuntos distintos

(retângulos tracejados), bem como a interação entre cada componente (fundo escuro).

Tal funcionamento segue uma sequência específica de ativação que garante a atualização

automática do modelo e é chamada, pelo autores da plataforma, de cadeia de ferramentas

(tool-chain). Explicam-se maiores detalhes sobre cada componente nas Subseções 2.6.1.1

a 2.6.1.4. Nesta última subseção, também é apresentada uma perspectiva geral da tool-

chain, que corresponde aos requisitos de responsividade para Rodin.

Figura 10: Arquitetura da Plataforma Rodin

Fonte: Abrial et al. (2010)

32

2.6.1.1 Plataforma Rodin

O conjunto mais básico de componentes da ferramenta é denominado de Plataforma

Rodin e é constituído de dois componentes básicos: Núcleo Rodin (Rodin Core) e Plata-

forma Eclipse. Esta refere-se à interface de programação básica do framework Eclipse. Já

o Núcleo Rodin está divido em duas partes: repositório e construtor. Ambos encontram-se

restritos e intimamente ligados à Plataforma Eclipse por meio dos padrões de codificação

Java disponibilizados pelo framework.

O repositório tem como principal funcionalidade a persistência de elementos do mo-

delo, seja em objetos Java ou em seus correspondentes no disco em arquivos XML. É

importante notar que o repositório não faz qualquer distinção sobre a representação das

informações a serem armazenadas. De fato, o componente é independente da sintaxe de

Event-B. Desta forma, é possível estendê-lo a possíveis modificações sintáticas posteriores,

necessárias aos objetos a serem persistidos.

O construtor escalona e dispara tarefas a serem executadas pela ferramenta, de acordo

com modificações ocorridas nos elementos contidos no repositório. O funcionamento do

construtor é definido pela plataforma Eclipse e pode também ser estendido a funcionali-

dades referentes a diferentes tipos de atualizações dos elementos do repositório.

2.6.1.2 Pacotes da biblioteca Event-B

Os dois pacotes definidos nesse conjunto de componentes são:

• Árvore de Sintaxe Abstrata de Event-B (Event-B Abstract Syntax Tree, AST): ne-

cessária para verificar a sintaxe da notação matemática utilizada na escrita de in-

variantes e guardas, por exemplo;

• Provador de Sequentes Event-B (Event-B Sequent Prover, SQP): motor de prova

que contém estruturas de dados, tais como a estrutura de sequente, regras de prova

e suporte a táticas (vide Subseção 2.6.1.3).

2.6.1.3 Núcleo Event-B

O Núcleo Event-B consiste dos componentes principais da cadeia de ferramentas da

plataforma, a saber: verificador estático (static checker, SC), gerador de obrigações de

prova (proof obligation generator, POG) e gerente de obrigações de prova (proof obligation

manager, POM ). A sincronia entre eles é gerenciada pelo construtor de Rodin.

33

O verificador estático é composto por analisadores léxico e sintático e verificador de

tipo, sendo responsável por dar retorno ao usuário por meio de mensagens de erro, bem

como por filtrar elementos do modelo que não estão habilitados para geração de obrigações

de prova. Isto é, basicamente, o verificador estático analisa máquinas e contextos em um

modelo, verificando erros sintáticos na notação matemática e a tipagem de variáveis e

fórmulas. POs são criadas apenas para os elementos do modelo (invariantes, guardas,

etc.) que não são reportados como errôneos pelo verificador.

O gerador de obrigações de prova é executado após a etapa de verificação estática. Há

vários requisitos de eficiência relacionados ao gerador para tornar a operação mais rápida.

Por exemplo, quando um evento de uma máquina é modificado, apenas as obrigações de

prova daquela máquina são recriadas. Cabe ao gerador executar simplificações na notação

matemática − o que facilita o processo de prova − , bem como permitir o rastreamento

dos componentes da PO à parte do modelo a que se refere.

O gerente de obrigações de prova integra as etapas do processo de prova. Para tanto,

este componente é responsável por rastrear provas e POs, e manter o status de uma prova

(descartada, revisada, pendente) atualizado. POM está divido em duas partes: extensível

(referente à geração de regras de prova) e estática (criação e manipulação da árvore de

prova). Conceitos tais como o de regras de prova são inerentes à criação de provas e, por-

tanto, encontram-se implementados no gerente de obrigações de prova. A implementação,

em Rodin, de alguns desses conceitos é discutida sucintamente a seguir:

• Regras de prova: uma regra de prova é um mecanismo que permite a transformação

de um sequente para criação da árvore de prova; em Rodin, o formato de regra é

expandido (em relação àquele definido na Seção 2.5) para, principalmente, permitir

reuso a um número maior de sequentes;

• Raciocinadores: geram regras de prova dado um sequente de entrada; a forma de

criação da regra não é verificada pelo POM, mas é necessário que seja logicamente

válida e que o racionador seja determinístico, isto é, gere a mesma saída (regra de

prova) sempre que receber uma mesma entrada;

• Táticas: conjuntos de estratégias de aplicação de raciocinadores e outras ferramen-

tas, usadas para construir e manipular árvores de prova; aplicam-se uma ou mais

táticas a um nó de uma árvore de prova com o objetivo de modificá-la; um tática

pode depender ou não de outras táticas, bem como ser configurada para aplicação

a nós específicos da árvore.

34

2.6.1.4 Interface do Usuário Event-B

A interface do usuário em Rodin é dividida em dois componentes: interface de mo-

delagem (Modeling User Interface, MUI) e interface de prova (Proving User Interface,

PUI ). Ambas são apresentadas por perspectivas na plataforma, o que permite ao usuário

alternar facilmente entre uma e outra (característica familiar ao desenvolvimento na pla-

taforma Eclipse). Os componentes de interface do usuário completam a tool-chain, cuja

interação entre componentes e ações básicas podem ser conferidas na Figura 11.

Figura 11: Cadeia de ferramentas em Rodin

Fonte: Abrial et al. (2010)

A interface de modelagem é ilustrada na Figura 12. Descrevem-se sucintamente as

seções mostradas a seguir:

• Navegador (explorer): permite acesso rápido aos projetos abertos, bem como às

máquinas e contextos, e aos seus componentes (variáveis, invariantes, etc.);

• Editor: é possível utilizar diferentes editores para escrever a especificação; há editores

padrão já instalados e outros que podem ser adquiridos via plug-in;

• Reportação de erros: essa seção reporta erros e problemas encontrados no modelo,

particularmente aqueles encontrados pelo verificador estático;

• Estrutura: resumo dos componentes da máquina ou contexto, com links para acesso

rápido;

• Símbolos: lista dos símbolos da linguagem matemática de Event-B, incluindo versão

ASCII.

A interface de prova é ilustrada na Figura 13. As seções dessa perspectiva são:

35

Figura 12: Perspectiva de modelagem em Rodin

• Árvore de prova: aplicam-se táticas automáticas ou manuais nos nós da árvore de

prova, transformando-a; o nó aparece em verde quando uma aplicação de tática é

bem-sucedida;

• Hipóteses: a lista de hipóteses do nó selecionado na árvore aparece nesta seção, em

que é possível escolher as proposições a serem utilizadas na prova;

• Objetivo: a conclusão do sequente a ser provado;

• Controle de prova: esta seção contém as diferentes ferramentas que podem ser utili-

zadas no processo de prova; de maneira geral, encontram-se as táticas (incluindo os

raciocinadores), ferramentas de seleção de hipóteses e simplificadores, além de um

prompt de comandos, onde é possível inserir instruções para prova manual;

• Navegador: acesso a máquinas, contextos, seus componentes e obrigações de prova.

2.7 Considerações finais

Este capítulo pretendeu servir de introdução a ambos Event-B e Plataforma Rodin.

Descreveram-se as características do processo de especificação e verificação formal com

Event-B (incluindo estrutura do modelo e linguagem matemática), permitindo correspon-

dência às funcionalidades presentes em Rodin para modelagem e prova. Apresentaram-se

36

Figura 13: Perspectiva de prova em Rodin

detalhes da ferramenta, tais como arquitetura e interface de interação, que podem ajudar

a situar onde se encaixam as contribuições aqui apresentadas, particularmente no que se

refere à perspectiva e processo de prova em Rodin. A seguir, no Capítulo 3, abordam-

se características da tecnologia de verificação formal objeto de estudo deste trabalho, os

solucionadores SMT.

37

3 Solucionadores SMT e o padrãoSMT-LIB

A questão de satisfatibilidade (SAT) é definida como um problema de decisão em que

dada um fórmula booleana de entrada, deve-se estabelecer se há uma interpretação que

a satisfaça, isto é, se existe um conjunto de atribuições de valores às variáveis da fórmula

que a torna verdadeira (modelo). Neste caso, diz-se que a fórmula é satisfatível ou, do

contrário, insatisfatível (BIERE et al., 2009).

Em diversos tipos de problema é necessário verificar a satisfatibilidade de fórmulas

considerando uma determinada teoria (ou combinação de teorias) subjacente que res-

trinja a forma como os símbolos contidos na fórmula são interpretados. Isto constitui o

problema de Satisfabilidade Módulo Teoria (SMT): avaliar se uma determinada fórmula

lógica fechada ϕ é satisfatível em relação a uma dada teoria T (BARRETT et al., 2009).

Um conceito intimamente associado ao de satisfatibilidade, e que é de fundamental

importância neste trabalho, é o de validade: verificar se uma determinada fórmula ϕ é

válida, ou seja, é verdadeira para todo conjunto de atribuições em T (BARRETT; STUMP;TINELLI, 2010b). Satisfatibilidade e validade são interdefiníveis, já que ϕ é válida se, e

somente se, sua negação for insatisfatível em T . Esta é justamente a aplicação de satisfa-tibilidade módulo teoria utilizada na verificação de obrigações de prova em Event-B: uma

PO H ` G, reescrita como H1∧H2∧ . . .∧Hn ⇒ G, pode ser provada válida verificando-sese H1 ∧H2 ∧ . . . ∧Hn ∧ ¬G é insatisfatível.

É possível verificar a validade de POs a partir de procedimentos SMT com o uso de

provadores automáticos, os solucionadores SMT. Estes podem utilizar um padrão de en-

trada de dados e linguagem de escrita de fórmulas comum denominado SMT-LIB. Ambos

os conceitos são descritos com mais detalhes nas Seções 3.1 e 3.2, a seguir.

38

3.1 Solucionadores SMT

Solucionadores SMT são provadores automáticos que lidam com o problema de Satis-

fatiblidade Módulo Teoria. Estas ferramentas têm sido aplicadas com sucesso a problemas

que vão de checagem de modelos à verificação estática de programas e modelagem. Há,

por exemplo, integração de solucionadores SMT em provadores de teoremas interativos

de lógica superior, sistemas de verificação e checagem estática (BARRETT et al., 2009).

Dois tipos de abordagem de implementação para solucionadores SMT têm apresen-

tado maior sucesso (BARRETT et al., 2009): abordagem gulosa (eager), em que traduz-se a

fórmula de entrada em uma fórmula proposicional equisatisfatível, utilizando consequên-

cias em T ; e abordagem preguiçosa (lazy), que consiste na integração de submódulos comprocedimentos de inferência especializados em teorias específicas, combinados a um núcleo

SAT.

O funcionamento padrão de um solucionador SMT atual baseia-se na combinação de

dois tipos básicos de procedimento (MOURA; BJORNER, 2011):

1. Solucionadores de teoria: procedimentos de decisão sobre a satisfatibilidade de con-

junções de literais, onde um literal é uma fórmula atômica ou a negação de uma;

2. Solucionadores SAT: procedimentos de satisfabilidade para lógica proposicional que

executam análise de casos para sub-fórmulas disjuntivas.

No núcleo SAT do solucionador, restringem-se as fórmulas às suas formas normais

conjuntivas (FNC ), isto é, cada fórmula consiste de uma conjunção de cláusulas, estas

constituídas de disjunções de literais. Por exemplo, a fórmula ¬p ∧ (q ∨ r) está em FNC.Neste caso, os únicos operadores proposicionais permitidos são conjunção, disjunção e

negação.

O procedimento de decisão utilizado na maioria dos provadores é a busca sistemática,

em que as escolhas sucessivas de atribuições de valores booleanos às variáveis da fórmula

são organizadas como uma árvore, onde cada nó representa uma variável e os vértices re-

presentam os valores verdadeiro ou falso para aquela variável. Um conjunto de atribuições

às variáveis da fórmula é, então, um caminho da raiz a uma folha da árvore. Um modelo

é encontrado quando o caminho torna a fórmula verdadeira. Grande parte dos provadores

baseados em busca utilizam o algoritmo DPLL (DAVIS; LOGEMANN; LOVELAND, 1962).

Parte do procedimento consiste na detecção de cláusulas conflitantes: cláusulas em que

39

cada atribuição de literal é falsa, o que serve para podar a árvore de escolhas, identificando

caminhos que não geram um modelo da fórmula.

A integração dos solucionadores SAT e de teorias geralmente ocorre criando-se uma

abstração proposicional da fórmula SMT, em que cada átomo é mapeado a uma variável

booleana (MOURA; BJORNER, 2011). Uma fórmula tida como satisfatível pelo núcleo SAT

induz um conjunto de literais. Estes são checados pelo solucionador de teoria, gerando

lemas de teoria (novas cláusulas) que são adicionados à fórmula de entrada. Esta é então

verificada novamente pelo solucionador SAT.

Determinadas aplicações SMT, como por exemplo a verificação de obrigações de prova

em Event-B, exigem uma combinação de teorias. Tal combinação pode ser realizada por

métodos estabelecidos, tais como o framework Nelson-Oppen (NELSON; OPPEN, 1979) para

combinar solucionadores de teoria com assinaturas disjuntas. Assinatura é o conjunto dos

símbolos de predicado e de função, com suas respectivas aridades. Para uma assinatura

Σ de determinada teoria T , ΣF representa o conjunto dos símbolos de função e ΣP oconjunto dos símbolos de predicado. Denominam-se símbolos constantes e proposicionais

os símbolos com aridade 0 em ΣF e ΣP , respectivamente. Fórmulas ϕ e termos t em Tsão constituídos dos símbolos em Σ.

Barrett et al. (2009) citam teorias de interesse comum em problemas SMT, a saber:

• Igualdade: conhecida como teoria de igualdade com funções não interpretadas, leva

em consideração o caso geral do problema de satisfatibilidade módulo teoria, isto

é, quando não há restrições em relação à interpretação dos símbolos em T ; nestateoria, existe um símbolo interpretado que é o predicado binário = (igualdade), que

deve satisfazer às propriedades clássicas de reflexividade, simetria, transitividade, e

"de Ackermann" (a = b⇒ f(a) = f(b)), para todas as funções, e (a = b⇒ (p(a)⇔p(b))) para todos os predicados;

• Aritmética: existem diversas teorias de interesse tais como inteira, real, linear e

não-linear, que podem ser utilizadas em diversas aplicações que vão de modela-

gem de conjuntos à manipulação de ponteiros e memória; solucionadores podem

implementar teorias aritméticas decidíveis, tais como a aritmética de Presburger

(PRESBURGER, 1931) e sua extensão com constantes não interpretadas;

• Vetores: teorias de vetores (arrays) são geralmente utilizadas para modelagem da

estrutura de dados vetor em programas ou para modelagem de memória; a satis-

fatibilidade de fórmulas sobre a teoria de vetores é NP-completa, mas há diversos

40

algoritmos para abordagem prática do problema;

• Vetores de bit de largura fixa: nestas teorias, constantes representam vetores de

bits, cada qual com uma largura associada; assinaturas podem incluir operadores

booleanos e aritméticos;

• Tipos de dados indutivos: assinaturas em primeira ordem de teorias para tipos de

dados indutivos associam símbolos de função a métodos construtores e seletores e

símbolos de predicado a testadores;

Algumas características associadas a solucionadores SMT são particularmente úteis

na abordagem do problema de verificação de obrigações de prova discutido neste tra-

balho, tornando esses provadores ainda mais atraentes em relação às soluções utilizadas

comumente. Tais funcionalidades incluem:

• Produção de modelos: vários solucionadores SMT têm a capacidade de reportar

modelos para fórmulas satisfatíveis, geralmente na forma de um conjunto de valores

atribuídos às variáveis;

• Produção de provas: a geração de provas para fórmulas insatisfatíveis é útil para,

por exemplo, certificação dos resultados do solucionador e determinação de hipóteses

relevantes para extração de núcleo insatisfatível (unsat-core);

• Identificação de núcleos insatisfatíveis: um núcleo insatisfatível de uma fórmula FNC

ϕ é um subconjunto, idealmente pequeno, insatisfatível de ϕ; em diversos provadores

a produção de unsat-cores está associada à funcionalidade de geração de provas.

3.2 SMT-LIB

SMT-LIB (BARRETT; STUMP; TINELLI, 2010a) é um padrão para solucionadores SMT,

constituído basicamente de uma linguagem de definição de termos e fórmulas, uma lingua-

gem de comandos para interagir com provadores compatíveis e de uma extensa biblioteca

de fórmulas lógicas para verificação de satisfatibilidade em relação a alguma teoria, os

benchmarks.

SMT-LIB surgiu como uma iniciativa à unificação do formato de entrada a ser utilizado

na escrita de benchmarks, facilitando o processo de avaliação na competição anual de solu-

cionadores SMT, a SMT-COMP (BARRETT; MOURA; STUMP, 2005). Em sua versão mais

41

recente (2.0, que é a considerada neste trabalho), SMT-LIB tem servido como uma espé-

cie de framework de uso, interface e caraterização de funcionalidades para solucionadores

SMT. SMT-LIB e SMT-COMP têm contribuído sensivelmente para o desenvolvimento da

tecnologia de Satisfatibilidade Módulo Teoria no decorrer dos anos.

Características de solucionadores SMT especificadas em SMT-LIB incluem (BAR-

RETT; STUMP; TINELLI, 2010b):

• Lógica subjacente: o padrão estabelece a lógica de primeira ordem com igualdade e

tipagem para escrita de expressões; isto significa que toda expressão válida em SMT-

LIB possui um tipo (sort) associado; é possível especificar tipos para cada símbolo,

bem como criar novos tipos com comandos SMT-LIB; é importante enfatizar que

em SMT-LIB não há distinção entre termos e fórmulas: fórmulas são termos de tipo

booleano;

• Teorias: SMT-LIB apresenta um catálogo de teorias usadas em solucionadores SMT

e uma linguagem de definição de assinaturas; conjuntos de expressões escritos em

SMT-LIB devem referir-se às teorias disponíveis;

• Entrada de fórmulas: a escrita de fórmulas leva em consideração a lógica básica do

padrão, mas é possível (por meio de uma linguagem específica em SMT-LIB) definir

sub-lógicas (ou simplesmente lógicas, na terminologia SMT-LIB), que restringem a

interpretação de expressões a subconjuntos dos símbolos da lógica e teoria subja-

centes;

• Interface: a linguagem de comandos SMT-LIB possui instruções diversas tais como

configuração de parâmetros nos solucionadores, asserção de fórmulas e recuperação

de provas e unsat-cores.

3.2.1 A linguagem SMT-LIB

Comandos e expressões SMT-LIB são escritos em scripts, que são interpretados pelos

solucionadores. Expressões num script SMT-LIB, bem como boa parte das saídas de um

solucionador compatível, consistem de expressões-S (listas entre parênteses) inspiradas na

linguagem Lisp.

Seja o script SMT-LIB na Figura 14 para verificar a validade da fórmula ((p ⇒q) ∧ (q ⇒ r)) ` (p⇒ r). Os comandos utilizados são explicados a seguir.

42

( set-option : p r in t− succe s s f a l s e )( set-logic QF_UF)( declare-fun p ( ) Bool )( declare-fun q ( ) Bool )( declare-fun r ( ) Bool )( assert (=> p q ) )( assert (=> q r ) )( assert ( not (=> p r ) ) )( check-sat )

Figura 14: Exemplo de script SMT-LIB

• Configurações do solucionador SMT: o comando set-option permite configurar o

provador, de acordo com opções implementadas (SMT-LIB define algumas confi-

gurações obrigatórias e outras opcionais); se o usuário tentar utilizar determinada

configuração e esta não tiver sido implementada para uso no solucionador, é possível

que a ferramenta reporte tal condição retornando como saída a palavra-reservada

unsupported; a opção :print-success recebe um de dois valores como argumento,

true ou false; por padrão esse valor é configurado como true, o que faz com que

haja saída do provador para cada comando executado com sucesso;

• Inicialização: o comando set-logic é único em cada script e indica a lógica a

ser utilizada; QF_UF é a lógica para fórmulas livres de quantificadores com funções

não interpretadas (Quantifier-Free Uninterpreted Functions); a Tabela 2 contém

exemplos de lógicas contidas no catálogo SMT-LIB;

• Declaração de funções: as constantes p, q e r são declaradas com o comando de

definição de funções declare-fun; este comando recebe o identificador da função

seguido da lista de parâmetros (vazia no caso de constantes) e tipo de retorno;

alternativamente, o comando define-fun define funções por meio de expressões de

função; o tipo Bool é pré-definido na lógica básica; novos tipos podem ser declarados

com o comando declare-sort; para tipos parametrizados e outros tipos definidos

por expressões, utiliza-se o comando define-sort;

• Asserções lógicas: a asserção de declarações é feita com o comando assert; os quanti-

ficadores forall e exists podem ser utilizados nas asserções (caso sejam suportados

pela lógica utilizada), bem como o binder let;

43

• Verificação de satisfatibilidade: o comando check-sat verifica se o conjunto de as-

serções é satisfatível; as saídas possíveis são sat, unsat ou unknown (vide Seção

4.3.3); para o exemplo, o resultado é unsat, indicando a validade da fórmula.

Tabela 2: Exemplos de lógicas em SMT-LIBIdentificador Descrição

QF_UF Incorpora a teoria básica e adiciona o tipoBool, sem quantificadores

AUFLIA Aritmética linear sobre inteiros com vetores,quantificadores, funções e tipos não interpretados

AUFNIRA Inclui reais à AUFLIAQF_IDL Aritmética de diferença sobre inteirosQF_BV Vetores de bit, sem quantificadoresQF_AX Vetores e booleanos, sem quantificadores

Expressões podem ser rotuladas com o símbolo reservado !. Por exemplo, a última

asserção (objetivo) do script exemplificado na Figura 14 pode ser anotada da seguinte

forma:

(assert (! (not (=> p r)) :named GOAL))

As funcionalidades de recuperação de atribuições booleanas e núcleo insatisfatível nos

solucionadores SMT (vide Seção 5.1) reportam, por padrão, apenas expressões rotuladas

presentes no script SMT-LIB.

Outros comandos úteis incluem: pop e push para manipulação da pilha global de as-

serções do solucionador SMT, o que serve para adicionar escopo às declarações de funções

e tipos e às asserções de fórmulas; e exit para finalizar o solucionador. Na Tabela 3 são

ilustrados os comandos disponíveis em SMT-LIB, de acordo com a sintaxe concreta do

padrão. Comandos contidos em um script seguem geralmente a seguinte ordem, adaptada

de Cok (2013):

1. Configurações com set-option

2. Inicialização com set-logic

3. Declarações de tipos e funções com declare/define-sort e declare/define-fun

4. Repetições de:

• push

44

• Prováveis novas declarações de tipos e funções

• Novas asserções

• check-sat

• pop

5. exit

Tabela 3: Comandos SMT-LIB

(set-logic )(declare-fun (*) )(define-fun (( )*) )(declare-sort )(define-sort (+) )(assert )(get-assertions)(check-sat)(get-proof)(get-unsat-core)(get-value +)(get-assignment)(push )(pop )(get-option )(set-option )(get-info )(set-info )(exit)

Fonte: Adaptado de Cok (2013)

3.3 Considerações finais

Neste capítulo foram discutidos fundamentos de solucionadores SMT, com o objetivo

de subsidiar o entendimento de como funciona o procedimento de verificação presente nos

provadores utilizados pelo plug-in SMT para Rodin. Além disso, explicitaram-se alguns

detalhes do padrão SMT-LIB, necessários para ajudar a entender, por exemplo, o me-

canismo de tradução de fórmulas da linguagem de Event-B para SMT-LIB presente no

45

plug-in. O Capítulo 4 contém detalhes de tal funcionalidade, bem como de todo o processo

de funcionamento do plug-in SMT para Rodin.

46

4 Integração de solucionadores SMTà Plataforma Rodin

Como exposto anteriormente no Capítulo 2, a Plataforma Rodin é extensível já que

sua construção segue o modelo de desenvolvimento do IDE Eclipse. Alcança-se tal ex-

tensibilidade por meio de complementos (plug-ins). De acordo com Eclipse (2011), um

plug-in integra-se ao ambiente juntamente com outros plug-ins e encapsula determinado

comportamento (funcionalidade).

O melhoramento do plug-in que adiciona à Rodin a funcionalidade de verificação de

obrigações de prova por meio de solucionadores SMT é o objetivo principal deste trabalho.

Faz-se necessário, então, expor as características do plug-in como forma de contextuali-

zação. No decorrer deste capítulo, apresentam-se uma discussão sobre a motivação para

a construção e aprimoramento do plug-in e um histórico de seu desenvolvimento, em que

são apresentados trabalhos relacionados ao aqui descrito. Adicionalmente, descrevem-se

as características principais da ferramenta.

4.1 Motivação

Déharbe (2013) esclarece que "o progresso nas técnicas de prova automática de teore-

mas é ponto chave para aumentar a eficácia, aplicação e disseminação de métodos formais"

e cita três formas de alcançar tal objetivo:

1. Algoritmos de verificação mais eficientes;

2. Melhor integração com os ambientes de desenvolvimento;

3. Suporte nativo a lógicas mais expressivas.

O autor enfatiza ainda que solucionadores SMT têm sido considerados como bons

candidatos no suprimento dos requisitos de eficácia e integração.

47

No Capítulo 3, citam-se aspectos de solucionadores SMT que ajudam a entender a

relevância do desenvolvimento deste tipo de ferramenta para a área de métodos formais,

especificamente na verificação de obrigações de prova. Particularmente, é possível citar a

capacidade dos solucionadores SMT de lidar com fórmulas extensas de lógica de primeira

ordem dada uma teoria subjacente, bem como a possibilidade de geração de provas e

contra-modelos como sendo características que permitem justificar a adoção e dissemina-

ção dessa categoria de provadores no campo de prova automática de teoremas.

Além disso, Déharbe et al. (2012) citam requisitos de usabilidade para a Plataforma

Rodin que podem ser supridos por solucionadores SMT:

• Automação: descarte (verificação) automático de obrigações de prova, diminuindo

assim a necessidade de intervenção do usuário por meio de provador interativo;

neste caso, de forma geral, o usuário deve prover manualmente as declarações e

asserções necessárias à prova da PO utilizando um prompt de comandos, o que

afeta negativamente a produtividade do processo;

• Informação: modificações em partes do modelo que não afetam uma obrigação de

prova já verificada não devem causar nova execução do provador; obrigações de

prova similares àquelas já provadas podem também ser provadas, caso detectadas;

fornecer contra-exemplos de obrigações de prova não verificadas automaticamente

de forma a ajudar o usuário a melhorar o modelo;

• Confiança: certificação do provador ou de suas saídas.

Assim, é possível considerar o desenvolvimento e aprimoramento do plug-in SMT para

Rodin como uma iniciativa importante na aplicação de solucionadores SMT no desenvol-

vimento formal de sistemas com Event-B.

Especificamente, visa-se com este trabalho otimizar o processo de verificação de POs

em Rodin: realizar prova interativa de obrigações de prova não verificadas automatica-

mente é uma atividade custosa e não-trivial para o usuário. Ao concentrar-se na busca

por retorno potencialmente útil quando uma PO é tida como inválida pela plataforma,

principalmente no tocante à reportação de contra-exemplos, as contribuições realizadas

possivelmente diminuem a necessidade de prova interativa. A ideia é que o usuário possa

se voltar a possíveis erros na especificação, corrigindo-a, ou ainda decidir sobre o uso de

tecnologias alternativas de verificação àquelas sendo utilizadas.

48

Adicionalmente, padronizar funcionalidades do plug-in para SMT-LIB pode ajudar

a melhorar a compatibilidade com um número maior de solucionadores, expandindo as

opções de verificação de POs, visto que tais provadores diferem um do outro em relação

à quantidade de teorias que suportam, entre outras características de eficácia e eficiência.

4.2 Histórico

No Capítulo 2, esclarece-se que o processo Event-B é baseado no método B de desen-

volvimento formal de software. A seguir são citados trabalhos que demonstram suporte

de solucionadores SMT na verificação de obrigações de prova geradas na aplicação de B.

A evolução destes trabalhos e, principalmente, o fato de ambos Event-B e B utilizarem

basicamente a mesma lógica − e, portanto, sendo necessário o suporte de provadores auto-

máticos − caracterizam parte do histórico e motivação para a integração de solucionadores

SMT na Plataforma Rodin.

4.2.1 SMT e Método B

Couchot et al. (2003) apresentam uma técnica de descarte automático de obrigações de

prova por meio de transformações de especificações B e posterior aplicação do provador

harVEy (DÉHARBE; FONTAINE, 2006). Em Tavares (2008) descreve-se a integração de

suporte à teoria de conjuntos em harVEy, possibilitando sua aplicação na verificação de

obrigações de prova produzidas pelo método B.

Gurgel et al. (2010) descrevem o pacote ZB2SMT que tem como objetivo integrar

ferramentas de apoio aos métodos B e Z, tais como Batcave (MARINHO et al., 2007) e

CRefine (OLIVEIRA; GURGEL; CASTRO, 2008), a solucionadores SMT. Os autores explicam

que a ferramenta integra os formalismos em B e Z e os traduz para SMT-LIB. Esta

tradução pode, então, ser utilizada como entrada de provadores compatíveis tais como

veriT (BOUTON et al., 2009).

Mentré et al. (2012) explicam uma outra abordagem de tradução de obrigações de

prova produzidas pelo método B, para viabilizar a verificação por meio de solucionadores

SMT. A técnica descrita envolve a conversão das POs para o formato de entrada do front-

end para provadores Why3 (FILLIÂTRE; PASKEVICH, 2013). Conchon e Iguernelala (2014)

apresentam modificações propostas ao solucionador Alt-Ergo (CONCHON; CONTEJEAN,

2008) com o objetivo de melhorar o desempenho deste na prova de POs do método B.

49

4.2.2 SMT e Event-B

Mais recentemente, iniciativas têm sido tomadas para prover suporte a solucionadores

SMT para uso com Event-B. Assim, este trabalho relaciona-se de forma mais direta àqueles

que descrevem o desenvolvimento do plugin SMT para a Plataforma Rodin. Os trabalhos

citados nesta seção serviram de embasamento para o restante deste capítulo.

Déharbe (2010) apresenta a ideia inicial de verificação de obrigações de prova produzi-

das no desenvolvimento com Event-B por meio de um solucionador SMT. São introduzidos

os aspectos de tradução da linguagem utilizada nas obrigações de prova para o formato

SMT-LIB. A formalização matemática também é apresentada. Um descrição expandida

da abordagem pode ser encontrada em Déharbe (2013). Enfatiza-se que o mecanismo de

tradução desenvolvido pode, potencialmente, ser aplicado também à classe de obrigações

de prova de B, Z, VDM e TLA+ (LAMPORT, 2001).

Apresenta-se uma descrição do trabalho voltado à implementação do plug-in em Al-

meida e Déharbe (2010). Os autores demonstram as características da versão até então

desenvolvida, como por exemplo o suporte ao provador veriT e sua versão estendida do

formato SMT-LIB. Um detalhamento da implementação da técnica de tradução com de-

finições macro pode ser encontrada em Almeida (2013).

Déharbe et al. (2012, 2014a, 2014b) descrevem a evolução do plug-in. Discutem-se

duas abordagens diferentes de tradução de sequentes Event-B para SMT-LIB. Explicam-

se ainda particularidades do comportamento interno de solucionadores SMT em relação

às fórmulas suportadas. A validação da proposta é feita por meio da verificação de um

número considerável de obrigações de prova advindas de projetos industriais e acadêmicos.

4.2.3 Retorno para obrigações de prova não descartadas em Ro-din

A ideia de prover feedback útil ao usuário quando uma PO em Rodin não é verifi-

cada pode ser encontrada também em trabalhos que utilizam o verificador de modelos e

animador ProB (LEUSCHEL; BUTLER, 2008) como um raciocinador.

Ligot, Bendisposto e Leuschel (2007) apresentam o ProB Disprover: um plug-in para

Rodin que faz uso do solucionador de restrições de ProB. O plug-in traduz sequentes

Event-B em uma máquina B, contendo as hipóteses e o objetivo a ser provado, além

de uma operação disprove, cuja pré-condição é formada pela conjunção das hipóteses e

a negação da conclusão. Após esta etapa de tradução, ProB é executado para tentar

50

encontrar um contra-exemplo da fórmula. Caso este seja encontrado, a PO é inválida

e o resultado é exibido na interface da plataforma. Esta versão da ferramenta, porém,

ainda não era capaz de ser utilizada como provador já que ProB apresentava limitações

relacionadas à manipulação de conjuntos infinitos ou não-enumerados e variáveis inteiras

de valor não estabelecido na especificação. Nestes casos, não encontrar um contra-exemplo

da fórmula não era garantia de que a PO era inválida.

Krings, Bendisposto e Leuschel (2014) descrevem a integração do rastreamento de

enumeração de conjuntos infinitos e busca exaustiva (funcionalidades implementadas em

ProB) ao Disprover, viabilizando seu uso como provador. Os autores avaliaram o plug-in,

comparando sua eficácia com a de outros provadores disponíveis para Rodin no descarte de

um conjunto de obrigações de prova. Demonstrou-se, como resultados, que ProB Disprover

é uma alternativa complementar aos provadores padrão de Rodin e ao plug-in SMT, já

que é capaz de descartar tipos diferentes de obrigações de prova em relação às táticas

comumente disponíveis. A respeito das diferenças de classe de POs, destaca-se que:

• Os provadores padrão de Rodin (PP, newPP e ML) são eficazes no descarte de POs

que contêm estruturas de teoria dos conjuntos e expressões relacionais;

• Solucionadores SMT apresentam melhores resultados que os outros provadores em

algumas POs com expressões aritméticas;

• ProB Disprover é mais bem aplicado a predicados sobre conjuntos enumerados e

apresenta suporte para aritmética de inteiros sobre domínios finitos.

4.3 Funcionamento e características

A sequência de funcionamento do plug-in SMT para Rodin pode ser resumida em

três etapas, relacionadas abaixo. Apresentam-se maiores detalhes sobre cada etapa nas

Subseções 4.3.1, 4.3.2 e 4.3.3. Uma visão esquemática da execução do plug-in é ilustrada

na Figura 15.

1. Tradução: Um sequente que representa determinada obrigação de prova é enviado

ao plug-in para ser traduzido da notação Event-B ao formato SMT-LIB;

2. Verificação: Um solucionador SMT é invocado para verificação da fórmula SMT;

3. Resposta: A resposta do solucionador (sat, unsat ou unknown) é enviada de volta

ao plug-in.

51

Figura 15: Visão esquemática do funcionamento do plug-in SMT para Rodin

Fonte: Déharbe et al. (2014a)

4.3.1 Tradução

A maior parte da notação encontrada nos sequentes Event-B possui correspondência

em SMT-LIB. Constantes e operadores booleanos, operadores relacionais e a maioria dos

símbolos aritméticos podem ser submetidos à tradução sintática direta. Os operadores de

divisão e exponenciação são traduzidos como símbolos não interpretados. Isto se deve a

divergências de tratamento desses operadores por diferentes provadores (ALMEIDA, 2013).

Por exemplo, o operador de divisão é representado por "/" em veriT e por div em Z3

(MOURA; BJORNER, 2008).

Para exemplificar a tradução de uma obrigação de prova para o formato SMT-LIB,

seja o seguinte sequente 0 < n ` n − 1 ∈ N e ambiente de tipo n : Z. O script SMTilustrado a seguir, na Figura 16, é criado como resultado da tradução. É importante notar

que o processo de transformação envolve a negação da conclusão do sequente. Isto acontece

52

porque o solucionador SMT deverá verificar a validade da obrigação de prova, isto é, a

insatisfatibilidade da fórmula negada.

( set-logic AUFLIA)( declare-fun n ( ) Int )( assert (< 0 n ) )( assert ( not (

53

( declare-fun A ( Int ) Bool )( declare-fun a ( ) Int )( define-fun ( par (X)

( union ( ( S1 (X Bool ) ) ( S2 (X Bool ) ) ) (X Bool )( lambda ( ( x X) ) ( or ( S1 x ) ( S2 x ) ) ) ) ) )

( define-fun enum ( ( x Int ) ) Bool (= x a ) )( assert ( not (= ( union A enum) A) ) )( check-sat )

Figura 17: Script SMT-LIB exemplificando tradução com expressões lambda

Fonte: Déharbe et al. (2014a)

O tradutor insere definições de funções, sendo a função enum a representação do con-

junto {a} e union a definição macro relativa à união de conjuntos. Uma lista destasdefinições, suportadas pelo plug-in, pode ser encontrada em Almeida (2013). Descrevem-

se detalhes do mecanismo de extensão a SMT-LIB para suporte a expressões lambda e

polimorfismo em Bonichon, Déharbe e Tavares (2014). Enfatiza-se ainda que veriT pode

gerar, em parte dos casos, uma fórmula de primeira ordem em SMT-LIB padrão para que

seja possível a verificaç