Sarah Raquel da Rocha Silva
BTS: Uma ferramenta de suporte ao desenvolvimento
de sistemas confiáveis baseados em componentes
Natal/RN
2013
Sarah Raquel da Rocha Silva
BTS: Uma ferramenta de suporte ao desenvolvimento
de sistemas confiáveis baseados em componentes
Dissertação apresentada ao Programa de
Pós-graduação em Sistemas e Computação
do Departamento de Informática e Matemática Aplicada da Universidade Federal do Rio
Grande do Norte, como requisito parcial para
a obtenção do grau de Mestre em Ciência da
Computação.
Orientador: Prof. Dr. Marcel Vinícius Medeiros Oliveira
Universidade Federal do Rio Grande do Norte
Centro de Ciências Exatas e da Terra
Departamento de Informática e Matemática Aplicada
Programa de Pós-graduação em Sistemas e Computação
Natal/RN
2013
Catalogação na fonte.
Ficha catalográfica elaborada pela Bibliotecária
Aline Nascimento Silva CRB 15/711
Silva, Sarah Raquel da Rocha.
BTS: uma ferramenta de suporte ao desenvolvimento de sistemas confiáveis
baseados em componentes / Sarah Raquel da Rocha. – Natal, RN, 2013.
81 f. : il.
Orientador: Dr. Marcel Vinícius Medeiros Oliveira
Dissertação (Mestrado) – Universidade Federal do Rio Grande do Norte.
Centro de Ciências Exatas e da Terra. Departamento de Informática e
Matemática Aplicada. Programa de Pós-Graduação em Sistemas e Computação.
1. Métodos formais – Dissertação. 2. Desenvolvimento baseado em
componentes – Dissertação. 3. Concorrência – Dissertação. 4. Verificação de
modelos – Dissertação. I. Oliveira, Marcel Vinícius Medeiros. II. Universidade
Federal do Rio Grande do Norte. III. Título
CDU: 004.4`2
BTS: Uma ferramenta de suporte ao desenvolvimento
de sistemas conáveis baseados em componentes
Sarah Raquel da Rocha Silva
Dissertação de Mestrado aprovada em 13 de dezembro de 2013 pela banca examinadora
composta pelos seguintes membros:
Prof. Dr. Marcel Vinícius Medeiros Oliveira (orientador) . . . . . . . . . . . . . . . DIMAp/UFRN
Profa. Dra. Anamaria Martins Moreira . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . DIMAp/UFRN
Prof. Dr. Alexandre Cabral Mota . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . UFPE
iii
Agradecimentos
A Deus, por ter me dado saúde e força para superar as dificuldades.
Ao professor Marcel, pela orientação e confiança.
Ao meu amigo, companheiro de trabalho e irmão na amizade Dalay, pelo carinho,
ajuda pessoal, psicológica e pela amizade que vai continuar presente em minha vida.
A Igor, por ter me dado apoio para entrar no mestrado, e por todo incentivo e carinho
para enfrentar e superar as dificuldades.
Aos meus pais (Rita e Francisco) e meus irmãos (Sérgio e Filipe), pelo amor, incentivo
e apoio incondicional. Por serem meu porto seguro, por sempre me apoiarem e por me
mostrarem que nenhum de nós nasce pronto, mas somos moldados pelas nossas escolhas.
A todos os amigos que me ajudaram direta ou indiretamente. A minha amiga de
infância Luciana, por ser sempre minha amiga de todas as horas. A meus companheiros
de laboratório Viviane, Ernesto, Sidney e Hélio, que fizeram parte dessa fase ao qual crie
laços que espero levar por toda minha vida.
A secretaria de pós-graduação da UFRN, que por intermédio da professora Fernanda
Nervo Raffin, me forneceu ajuda financeira durante essa fase.
A todos vocês, o meu muito obrigada.
iv
Resumo
O desenvolvimento de sistemas baseados em componentes revolucionou o processo de
desenvolvimento de software, facilitando a manutenção, trazendo mais confiabilidade e
reutilização. Porém, mesmo com todas as vantagens atribuídas ao componente, é necessário uma análise detalhada de sua composição. Realizar verificação a partir de testes
de software não é o suficiente para se ter uma composição segura, pois esses não são
baseados em modelos semânticos formais nos quais podemos descrever precisamente o
comportamento do sistema. Nesse contexto, os métodos formais oferecem a possibilidade de especificarmos sistemas de forma precisa, através de notações com forte base
matemática, trazendo, entre outros benefícios, mais segurança. O método formal CSP
possibilita a especificação de sistemas concorrentes e verificação de propriedades inerentes
a tais sistemas, bem como refinamento entre diferentes modelos. Existem abordagens que
aplicam restrições usando CSP, para verificar o comportamento da composição entre componentes, auxiliando a verificação desses componentes antecipadamente. Visando auxiliar
esse processo, tendo em vista que o mercado de software busca cada vez mais automação,
minimizando trabalhos e trazendo agilidade nos negócios, este trabalho apresenta uma ferramenta que automatiza a verificação da composição entre componentes, onde o conjunto
de verificações CSP impostas é gerado e verificado internamente, oculto para o usuário.
Dessa forma, através de uma interface simples, a ferramenta BTS (BRIC-Tool-Suport)
ajuda a criar e compor componentes, prevendo, com antecedência, comportamentos indesejáveis no sistema, como deadlocks.
Keywords: Métodos Formais, Desenvolvimento Baseado em Componentes, Concorrência, Verificação de Modelos.
v
Abstract
The component-based development of systems revolutionized the software development
process, facilitating the maintenance, providing more confiability and reuse. Nevertheless,
even with all the advantages of the development of components, their composition is an
important concern. The verification through informal tests is not enough to achieve a
safe composition, because they are not based on formal semantic models with which we
are able to describe precisally a system’s behaviour. In this context, formal methods
provide ways to accurately specify systems through mathematical notations providing,
among other benefits, more safety. The formal method CSP enables the specification
of concurrent systems and verification of properties intrinsic to them, as well as the
refinement among different models. Some approaches apply constraints using CSP,
to check the behavior of composition between components, assisting in the verification
of those components in advance. Hence, aiming to assist this process, considering
that the software market increasingly requires more automation, reducing work and
providing agility in business, this work presents a tool that automatizes the verification
of composition among components, in which all complexity of formal language is kept
hidden from users. Thus, through a simple interface, the tool BST (BRIC-Tool-Suport)
helps to create and compose components, predicting, in advance, undesirable behaviors in
the system, such as deadlocks.
Keywords: Formal Methods, Component-Based Development, competition, Model
Checking.
vi
Sumário
Lista de Figuras
p. viii
Lista de Tabelas
p. xi
1 Introdução
p. 1
1.1
Visão Geral . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 1
1.2
Motivação . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 2
1.2.1
Proposta . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 3
1.2.2
Trabalhos Relacionados . . . . . . . . . . . . . . . . . . . . . . .
p. 4
Objetivos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 5
1.3.1
Objetivos Gerais . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 5
1.3.2
Objetivos Específicos . . . . . . . . . . . . . . . . . . . . . . . .
p. 5
Estrutura da Dissertação . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 6
1.3
1.4
2 Fundamentação Teórica
p. 7
2.1
Sistemas Baseados em Componentes . . . . . . . . . . . . . . . . . . .
p. 7
2.2
CSP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 9
2.3
2.2.1
Semântica CSP . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 13
2.2.2
Ferramentas para CSP . . . . . . . . . . . . . . . . . . . . . . .
p. 18
Abordagem para o desenvolvimento sistemático de sistemas confiáveis .
p. 22
3 Uma verificação formal para desenvolvimento de sistemas confiáveis baseados em
componentes
p. 36
3.1
p. 36
Análise CSP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Sumário
vii
4 BTS: Ferramenta de suporte ao desenvolvimento de sistemas confiáveis baseados
em componentes
p. 46
4.1
Detalhes Técnicos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 46
4.2
Ferramenta BTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 47
4.2.1
Aplicação prática da estratégia pela BTS . . . . . . . . . . . . .
p. 55
4.2.2
Considerações Finais . . . . . . . . . . . . . . . . . . . . . . . .
p. 64
p. 65
5 Estudo de Caso
5.1
Buffer Circular . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 65
5.2
Aplicação do Buffer Circular na BTS . . . . . . . . . . . . . . . . . . .
p. 68
5.2.1
Contrato BRIC de Cell e Controller
. . . . . . . . . . . . . . .
p. 68
5.2.2
Composição . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 70
Análise do Estudo de Caso . . . . . . . . . . . . . . . . . . . . . . . . .
p. 74
5.3
6 Considerações finais
6.1
Trabalhos Futuros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Referências Bibliográficas
p. 76
p. 77
p. 78
viii
Lista de Figuras
2.1
Atividades Para o Desenvolvimento com Componentes . . . . . . . . .
p. 8
2.2
Exemplo de especificação CSP . . . . . . . . . . . . . . . . . . . . . . .
p. 10
2.3
Máquina de estado do processo PARQUE criada pelo FDR2 . . . . . . .
p. 15
2.4
Processos PORTAO1 e PORTAO2 com seus estados e suas recusas . . .
p. 16
2.5
Processos divergentes . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 17
2.6
Interface da FDR2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 20
2.7
Interface da ProBe . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 20
2.8
Interface da ProB . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 21
2.9
Modelo de componente . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 22
2.10 Exemplo de um Cliente-Servidor . . . . . . . . . . . . . . . . . . . . . .
p. 23
2.11 Descrição dos tipos e canais . . . . . . . . . . . . . . . . . . . . . . . .
p. 23
2.12 Descrição do comportamento do componente Cliente . . . . . . . . . .
p. 23
2.13 Descrição do comportamento do componente Máquina . . . . . . . . .
p. 23
2.14 Protocolo do Cliente para o canal maq . . . . . . . . . . . . . . . . . .
p. 26
2.15 Protocolo da Maquina para o canal maq . . . . . . . . . . . . . . . . .
p. 27
2.16 Dual-protocol de Prot_Cliente . . . . . . . . . . . . . . . . . . . . . . .
p. 28
2.17 Reutilização de componente . . . . . . . . . . . . . . . . . . . . . . . .
p. 28
2.18 Criando um novo componente Máquina . . . . . . . . . . . . . . . . . .
p. 29
2.19 Exemplo de comunicação via Buffer . . . . . . . . . . . . . . . . . . . .
p. 29
2.20 Canais desacoplados . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 31
2.21 Compatibilidade de Auto-Injeção com Buffer . . . . . . . . . . . . . . .
p. 31
2.22 Exemplo de três regras de composição . . . . . . . . . . . . . . . . . . .
p. 31
Lista de Figuras
ix
4.1
Diagrama de Caso de Uso da BTS . . . . . . . . . . . . . . . . . . . . .
p. 47
4.2
Diagrama de sequência da criação de tipos . . . . . . . . . . . . . . . .
p. 48
4.3
Interface para criação de tipos . . . . . . . . . . . . . . . . . . . . . . .
p. 49
4.4
Interface para criação de canais . . . . . . . . . . . . . . . . . . . . . .
p. 49
4.5
Diagrama de sequência da criação de contrato . . . . . . . . . . . . . .
p. 50
4.6
Interface para criação de contrato . . . . . . . . . . . . . . . . . . . . .
p. 51
4.7
Tela de resultado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 51
4.8
Tela de instanciação . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 52
4.9
Diagrama de sequência da composição . . . . . . . . . . . . . . . . . .
p. 53
4.10 Tela de Composição . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 53
4.11 Estrutura da BTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 54
4.12 Entradas e saídas da BTS . . . . . . . . . . . . . . . . . . . . . . . . .
p. 54
4.13 Interface BTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 55
4.14 Exemplo de comportamento do componente . . . . . . . . . . . . . . .
p. 57
4.15 Interface de saída do TypeChecker . . . . . . . . . . . . . . . . . . . . .
p. 57
5.1
Buffer Circular . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 66
5.2
Representação do componente Cell . . . . . . . . . . . . . . . . . . . .
p. 66
5.3
Representação do componente Controller . . . . . . . . . . . . . . . . .
p. 66
5.4
Interface para descrição de eventos de entrada e saída . . . . . . . . . .
p. 69
5.5
Interface para descrição protocolo e dual-protocols . . . . . . . . . . . .
p. 71
5.6
Tela de composição com o exemplo da composição em interleave . . . .
p. 71
5.7
Composição em interleave de Cell1 e Cell2 . . . . . . . . . . . . . . . .
p. 72
5.8
Composição em interleave de Cell1, Cell2 e Cell3 . . . . . . . . . . . .
p. 72
5.9
Composição em Communication do Controller com as Células . . . . .
p. 73
5.10 Composição em feedback do componente resultante das células com o
Controller . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 73
Lista de Figuras
x
5.11 Composição em reflexive do componente resultante da composição em
feedback . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
p. 74
xi
Lista de Tabelas
2.1
Operadores da linguagem CSP . . . . . . . . . . . . . . . . . . . . . . .
p. 11
3.1
Teste de Caracterização da Composição em Interleave . . . . . . . . . .
p. 37
1
1
Introdução
Neste capítulo apresentaremos uma visão geral e os fatores motivadores desta dissertação, além da proposta e objetivos que buscamos alcançar. Por fim, apresentaremos a
estrutura que segue este documento, descrevendo o que será visto em cada capítulo.
1.1
Visão Geral
A engenharia de software surgiu como uma forma de organizar e gerenciar o desenvolvimento de software [WIRTH, 2008]. Esta preocupa-se com todos os aspectos de produção
do sistema, desde a especificação inicial, passando pela implementação, implantação e manutenção.
Cada vez mais buscam-se características que melhorem a qualidade do software, como
maior facilidade de manutenção, confiabilidade e reutilização. Uma grande ideia que
revolucionou o processo de desenvolvimento foi compor o sistema em pequenos pedaços
que chamamos de componentes [MCILROY, 1968], descritos em [SZYPERSKI, 2002] da
seguinte forma: "Um componente de software é uma unidade de composição com interfaces
especificadas através de contratos e dependências de contexto explícitas. Um componente
de software pode ser distribuído independentemente e está sujeito a composição com outras
partes".
O desenvolvimento de sistemas baseados em componentes (SBC)[SPAGNOLI; BECKER, 2003] estabelece uma integração entre os componentes de software, que facilitam o
acréscimo de novas funcionalidades, a manutenção e a substituição dos componentes existentes. Porém, mesmo com todas as boas características atribuídas ao desenvolvimento
baseado em componentes, estes devem ser compostos de forma segura, principalmente
quando lidamos com sistemas críticos. Um sistema de aviação, por exemplo, deve ter alta
confiabilidade para que em caso de falha, continue operando normalmente [MOTA et al.,
2010].
1.2 Motivação
2
Uma característica importante para obter sucesso no desenvolvimento de um componente é verificar adequadamente suas funcionalidades. Hoje, a prática mais utilizada
para essa verificação ainda é o teste de software. Porém, garantir a qualidade do software
apenas com inspeções informais é muito difícil, principalmente quando lidamos com software complexos. Nesse contexto, surgem os métodos formais, os quais constituem outro
grande avanço em direção à construção de software de qualidade. Através de linguagens
formais, as quais possuem uma base matemática, os desenvolvedores especificam o sistema mantendo a precisão da especificação. Além disso, estas linguagens possuem uma
semântica formal, através da qual é possível realizar provas matemáticas para verificar
características como, por exemplo, a ausência de deadlocks.
CSP [HOARE, 1985] é um método formal que permite a modelagem e verificação
formal de sistemas concorrentes. Ele possui um conjunto de ferramentas e alguns trabalhos na literatura [HOARE, 1985] [ROSCOE et al., 1997] [SCHNEIDER, 1999]. A
linguagem CSP é baseada em processos que se comunicam através de eventos (ações) e
esses representam o fluxo do seu comportamento. A linguagem também possui modelos
semânticos, os quais permitem a verificação e comparação entre processos. As ferramentas que dão suporte a CSP auxiliam tanto no processo de modelagem e verificação, como
na visualização gráfica do comportamento do processo. São exemplos dessas ferramentas,
o FDR2 [BROWNLEE, 2000], proBE [PROBE. . . , 2003] e TypeChecker 1 . Além dessas,
CSP ainda dispõe do provador de teorema CSP-Prover [ISOBE; ROGGENBACH, ]. Este
é uma integração das teorias de CSP com o provador de teorema Isabelle [NIPKOW et
al., 2002].
Por todas essas características e suporte de ferramentas, CSP tem ganho muita importância nos últimos tempos, com grandes aplicações na indústria [NOGUEIRA et al.,
2008] [FEITOSA et al., 2008] [PERES; MOTA, 2007] [NETO, 2007]. Atualmente, seus
benefícios vêm sendo explorados junto à área de testes para uma melhor geração e automação dos testes de software [BERTOLINI; MOTA, 2008] [CAVALCANTI; GAUDEL,
2007] [NOGUEIRA et al., 2008] [NETO, 2007].
1.2
Motivação
No processo de desenvolvimento baseado em componentes é importante uma análise
detalhada de como esses se integram no sistema, não bastando apenas verificar o compo1 http://www.fsel.com/software.html
1.2 Motivação
3
nente, mas também sua composição. A falta de uma verificação adequada da composição
entre esses componentes pode gerar problemas como deadlocks, os quais ocorrem quando
os componentes ficam impedidos de continuar suas execuções, pois cada um fica bloqueado
aguardando o outro. Nesse sentido, é preciso fazer com que os componentes se integrem
de forma que consigam se comunicar adequadamente. Uma abordagem ideal deveria prever esses comportamentos com antecedência. Linguagens formais, como CSP, podem ser
utilizadas com esta finalidade.
Em [RAMOS, 2011] é descrita uma estratégia que propõe a composição sistemática
e segura de componentes baseada na linguagem formal CSP. A estratégia define quatro
regras de composição: interleave, communication, feedback e reflexive, as quais asseguram
a ausência de deadlocks no componente resultante da composição.
A abordagem, a ser descrita mais detalhadamente no Capítulo 2, baseia-se em um
modelo de componentes que impõe as restrições necessárias para uma interação segura. As
regras oferecem um método sistematizado para preservar propriedades comportamentais
por construção. Com isso é possível identificar, através de propriedades conhecidas do
sistema, comportamentos da composição entre componentes antes de sua implementação.
1.2.1
Proposta
A abordagem proposta em [RAMOS, 2011] apresenta características de grande importância para verificação da composição entre componentes. Porém, o mercado de software
busca automação de processos [GROOVER, 2007]. Assim sendo, a aplicação de um método, como o proposto em [RAMOS, 2011], na prática, exige ferramentas que facilitem
sua utilização, auxiliando o usuário e trazendo agilidade ao desenvolvimento.
Este trabalho apresenta o desenvolvimento de uma ferramenta de apoio à estratégia proposta em [RAMOS, 2011], visando facilitar sua utilização. A ideia é abstrair a
complexidade imposta pelos modelos formais. Como benefícios, a ferramenta trará um
método de verificação prático, com agilidade no processo de desenvolvimento. Para isso,
a avaliamos através de um estudo de caso.
A seguir apresentaremos algumas abordagens e ferramentas voltadas para o desenvolvimento baseado em componentes.
1.2 Motivação
1.2.2
4
Trabalhos Relacionados
São muitos os trabalhos publicados que apresentam modelos de desenvolvimento baseado em componentes [LAU; NTALAMAGKAS, 2009] [LAU et al., 2011] [LAU et al.,
2005] [BARN; BROWN, 1998]. Existem alguns voltados para a verificação de componentes, como o proposto em [MARCILON, 2012] que apresenta a descrição de um processo de
derivação e verificação de propriedades de componentes nas nuvens. O processo envolve
a especificação formal do comportamento do componente por meio de contratos descritos
pela linguagem Circus [WOODCOCK; CAVALCANTI, 2002]. Esse contrato é refinado e
traduzido, chegando à implementação de um componente. Essa proposta tem em comum
com a abordagem descrita em [RAMOS, 2011] o fato que ambos conseguem verificar com
antecedência o comportamento do componente, devido à utilização de modelos formais.
Existem algumas ferramentas voltadas para verificação funcional automática de componentes. Em [BARBOSA, 2005] é descrita uma ferramenta que gera, executa e analisa
os resultados de testes funcionais para componentes de software a partir de especificações UML [RUMBAUGH et al., 2004] e restrições OCL [WARMER; KLEPPE, 2003].
Em nossa ferramenta, essa verificação é voltada para análise formal da composição entre
componentes.
Podemos encontrar em [EASSA; ABULNAJA, 2001] a proposta de um conjunto de
sub-ferramentas que auxiliam na construção de sistemas baseados em componentes, através da descrição de casos de uso em UML [RUMBAUGH et al., 2004]. Em nossa ferramenta, o desenvolvimento dos componentes é baseado na descrição de um modelo de
componente usando características da linguagem formal CSP.
O conjunto de ferramentas VEST [STANKOVIC et al., 2003] apoia o desenvolvimento
distribuído de sistemas embarcados baseados em componentes, cujo objetivo é fornecer
um conjunto de verificação de dependências baseado nos conceitos de aspecto [KICZALES
et al., 2001] para lidar com problemas não funcionais. Nossa ferramenta lida com a
verificação de segurança para problemas de deadlocks, baseado em características dos
componentes.
O projeto CESAR [JOLLIFFE, 2010] também investiu em ferramentas para o desenvolvimento de sistemas baseados em componentes. A ferramenta X-MAN [LAU; TRAN,
2012] é uma ferramenta industrial para o desenvolvimento de sistemas embarcados, automotivos e aviônicos. A ferramenta utiliza uma engenharia dirigida por modelo (MDE)
através da ferramenta GME (Ambiente de modelo genérico) [LEDECZI et al., 2001].
1.3 Objetivos
5
Em [MATSUMOTO; FUTATSUGI, 2000b] é proposta uma ferramenta que assegura
uma alta confiabilidade no desenvolvimento de sistemas baseados em componentes. O
desenvolvimento da ferramenta foi baseado na arquitetura em árvore [MATSUMOTO;
FUTATSUGI, 2000a]. Ela recebe como entrada uma especificação dos requisitos do software e uma especificação refinada de como combinar os componentes, que é descrita através da linguagem de especificação CafeOBJ [DIACONESCU; FUTATSUGI, 1998]. Além
disso, são especificados os componentes javaBeans (componentes descritos através da linguagem Java). Como saída a ferramenta apresenta um componente que é resultado dos
componentes descritos na entrada, juntamente com os conectores. A alta confiabilidade é
garantida através da verificação dos requisitos e geração da conexão entre os componentes de forma automática. Esse trabalho possui características bem parecidas com nossa
proposta, levando-se em consideração a confiabilidade imposta através da verificação realizada a partir de linguagens formais. Nessa ferramenta, a conexão entre os componentes é
gerada automaticamente, de acordo com a especificação descrita na entrada. Já na nossa
esse comportamento é invertido, onde a descrição da conexão é realizada manualmente,
bem como o comportamento do componente, e ela gera automaticamente o conjunto asserções de verificação.
1.3
Objetivos
1.3.1
Objetivos Gerais
O objetivo geral desse trabalho consiste no desenvolvimento de um ambiente automatizado para verificação da composição entre componentes. Esse ambiente auxiliará
o usuário na verificação e prevenção de comportamentos indesejáveis da interação entre
componentes.
1.3.2
Objetivos Específicos
São objetivos específicos deste trabalho:
• Investigar a existência de ferramentas para verificação de componentes. Fizemos
um levantamento na literatura em busca de ferramentas voltadas para verificação
do componente e de sua composição. A maioria dos trabalhos encontrados trata
da criação e verificação do componente em si, e poucas utilizam modelos formais.
Nossa ferramenta se preocupa não só com a descrição e criação do componente, mas,
1.4 Estrutura da Dissertação
6
principalmente, da verificação de sua composição a partir de várias propriedades
descritas através da especificação formal CSP.
• Estudar a verificação formal da abordagem proposta. Em [OLIVEIRA, 2012b] foi
realizada uma análise formal a partir da implementação das regras e restrições proposta em [RAMOS, 2011]. Nesse estudo, conseguimos identificar comportamentos
e extrair características necessárias para a implementação de nossa ferramenta.
• Desenvolver ferramenta de apoio. Nessa etapa foi desenvolvida a ferramenta que
automatiza a abordagem proposta em [RAMOS, 2011]. Para implementação utilizamos a linguagem java e a IDE NetBeans. Além disso, a fim de realizar as verificações necessárias nos scripts CSP gerados, foram integradas outras duas ferramentas
de suporte CSP: TypeChecker e FDR2.
• Validar a ferramenta. Através da aplicação da estratégia, utilizando a ferramenta
em um estudo de caso proposto em [OLIVEIRA, 2012b]. Nesta aplicação, analisamos se, de fato, a especificação descrita manualmente no estudo de caso é gerada
automaticamente e corretamente pela ferramenta, sendo possível extrair características como: interface amigável, melhor entendimento, facilidade de uso e redução
da complexidade.
1.4
Estrutura da Dissertação
No Capítulo 2 é feita uma breve introdução ao desenvolvimento baseado em componentes. Em seguida, apresentamos a linguagem CSP, onde descrevemos sua sintaxe, seus
modelos semânticos e apresentamos as ferramentas de suporte ao método. Finalizamos
com uma descrição da estratégia proposta em [RAMOS, 2011], onde apresentamos as
regras e restrições necessárias para se obter composições seguras. No Capítulo 3 apresentamos uma análise CSP da estratégia proposta em [RAMOS, 2011], através da ferramenta
FDR2, que constitui a base para construção de nossa ferramenta. No Capítulo 4, apresentamos toda estruturação de nossa ferramenta, como detalhes técnicos e funcionalidade.
O Capítulo 5 apresenta o estudo de caso que foi desenvolvido no decorrer desse trabalho
de dissertação. Concluímos esse trabalho com as considerações finais e trabalhos futuros.
7
2
Fundamentação Teórica
Neste capítulo serão apresentados os conceitos necessários para o entendimento desse
trabalho. Começaremos explicando os conceitos fundamentais de sistemas baseados em
componentes. Logo em seguida serão apresentados os conceitos da linguagem CSP, seus
modelos semânticos clássicos e as ferramentas de apoio à linguagem. Finalizaremos com
a descrição da abordagem utilizada como base nesse trabalho.
2.1
Sistemas Baseados em Componentes
O desenvolvimento de sistemas baseados em componentes surgiu da necessidade de se
melhorar o processo de desenvolvimento de software, tendo como motivação a busca pelo
aumento da produtividade, da qualidade e da redução nos custos do software, trazendo
com isso novas perspectivas para o desenvolvimento [VINCENZI et al., 2005].
Existe um grande interesse no desenvolvimento de software através da integração planejada de componentes existentes [BROWN; WALLNAU, 1998]. Com o desenvolvimento
baseado em componentes, sistemas que antes eram construídos em um único módulo,
agora são divididos em várias partes, onde cada uma representa uma funcionalidade do
sistema. Esse processo possui muitas vantagens, entre elas podemos citar a reutilização e
manutenção de componentes [VINCENZI et al., 2005].
A ideia de componente de software não é novidade. Em 1968 McIlroy já acreditava no futuro da indústria de componentes de software reutilizáveis [MCILROY, 1968].
Na literatura podemos encontrar várias definições de componentes. A definição que mais
assemelha-se a nosso trabalho foi proposta em [SZYPERSKI, 2002] e define o componente
de software como uma unidade de composição com interfaces contratualmente especificadas, podendo ser usado independentemente e combinado com outras partes.
No desenvolvimento de sistemas baseados em componentes, podemos considerar duas
características: o desenvolvimento de componentes e o desenvolvimento com componentes.
2.1 Sistemas Baseados em Componentes
8
O desenvolvimento de componentes representa a sua implementação. Já no desenvolvimento com componentes, considera-se a existência destes e os relacionam as atividades
necessárias para sua composição no sistema.
Segundo [BROWN; SHORT, 1997] existem as seguintes atividades essenciais para o
desenvolvimento com componentes: 1) encontrar componentes; 2) selecionar componentes; 3) realizar adaptações; 4) realizar a composição dos componentes; e 5) atualizar os
componentes. A Figura 2.1 ilustra essas atividades.
Figura 2.1: Atividades Para o Desenvolvimento com Componentes
Na primeira atividade são selecionados componentes com potencial para serem usados
no desenvolvimento do sistema. A atividade de seleção deve garantir que o componente
selecionado execute as funcionalidades necessárias para a aplicação. A adaptação consiste
em corrigir potenciais fontes de conflitos entre componentes selecionados para compor o
sistema. A atividade de composição utiliza uma infraestrutura comum para a realização
da composição dos componentes. Por último, a atividade de atualização consiste na substituição de versões antigas por novos componentes. Esta tem um impacto muito grande,
pois uma alteração no componente sem um planejamento pode acarretar comportamentos
inesperados em outros componentes do sistema.
Nierstrasz e Dami definem a composição de componentes como “o processo de construir aplicações por interconectar componentes de softwares através de seus plugins” [NIERSTRASZ; DAMI, 1995]. Esses plugins definem o meio de interação e comunicação entre
os componentes. Em [RAMOS, 2011], essa interação é descrita no modelo de componente,
o qual chamamos de contrato. Um contrato de componente descreve o comportamento
que o mesmo deve ter para se comportar de maneira confiável. Nesse sentido, métodos
formais tornam-se uma ferramenta importante, visto que eles permitem a formalização
e verificação de consistência dos componentes e seus contratos, trazendo assim um alto
grau de confiabilidade ao componente resultante.
A geração de contrato não está apenas associada à confiabilidade de um componente,
2.2 CSP
9
mas também à confiabilidade da composição desses componentes. O trabalho proposto
em [RAMOS, 2011], que está sendo abordado nesta proposta de dissertação, define regras
para compor componentes de forma segura, que são baseadas em um modelo de contrato.
Ainda nesse capítulo, você encontrará mais informações sobre essa abordagem.
2.2
CSP
CSP [HOARE, 1978] é uma linguagem formal que descreve o sistema em termos
de processos. Esses processos operam independentemente e interagem com os outros
através de ações (eventos). CSP é suportada por uma teoria matemática, um conjunto
de ferramentas de prova e alguns trabalhos literários [HOARE, 1985] [ROSCOE et al.,
1997] [SCHNEIDER, 1999]. Sua abordagem tem sido utilizada para especificação, análise
e verificação de sistemas concorrentes e em tempo real [SCHNEIDER, 1999]. Nessa seção
apresentaremos algumas características e operadores da linguagem, mais especificamente,
aqueles que fazem parte do contexto desse trabalho.
A Figura 2.2 apresenta um exemplo de especificação utilizando uma notação funcional
chamada CSPM , o qual tomaremos como base para apresentar os conceitos da linguagem.
A especificação descreve o comportamento de entrada em um parque de diversões. O
parque possui os clientes e um CAIXA que recebe o dinheiro, entrega o bilhete e o troco.
Outros comportamentos serão apresentados de acordo com a descrição da linguagem.
Iniciamos os conceitos de CSP apresentando a descrição de tipos e canais. Na linguagem, tipos compreendem conjuntos de valores e operações que podem ser realizados
sobre estes valores. Estes podem ser descritos, por exemplo, como inteiros, intervalos,
booleanos, entre outros. Na especificação da Figura 2.2 temos o exemplo da declaração de um tipo intervalo que representa o valor a ser pago na entrada do parque. CSP
também permite a criação de novos tipos através da palavra reservada datatype, onde
seus conjuntos de valores não fazem parte dos valores já definidos pela linguagem e são
representados como tipos enumerados ou uma união disjunta. Em nossa especificação
definimos o tipo ALFA que é representado por três valores (datatype ALFA = a | b
| c), onde a, b e c representam os clientes do sistema.
Os canais representam as portas de comunicação ou simplesmente a ação do processo, a qual damos o nome de evento. Na Figura 2.2 podemos encontrar a declaração
de alguns canais como dinheiro, bilhete e troco que definem ações no comportamento do processo CAIXA. Estes comunicam valores do tipo ALFA, tal que dinheiro.a
2.2 CSP
10
Valor ={0..10}
datatype ALFA = a | b | c
channel entrar, brincar, sair
channel dinheiro, bilhete, troco, moeda, passe : ALFA
channel entrada : Valor
PARQUE = entrar -> brincar -> sair -> PARQUE
CAIXA = dinheiro?clt -> bilhete!clt -> troco!clt -> CAIXA
USUARIOS = USUARIO(a) ||| USUARIO(b) ||| USUARIO(c)
USUARIO(clt) =
((entrar -> moeda!clt ->
(passe.clt -> troco.clt -> SKIP
[] troco.clt -> passe.clt -> SKIP)); brincar -> sair -> USUARIO(clt))
|~|
((moeda!clt -> entrar ->
(passe.clt -> troco.clt -> SKIP
[] troco.clt -> passe.clt -> SKIP)); brincar -> sair -> USUARIO(clt))
ENTRADA_PARQUE =
entrada?x ->
if (x==8) then SISTEMA_PARQUE else ENTRADA_PARQUE
MAQUINA = CAIXA [[dinheiro <- moeda, bilhete <- passe]]
SISTEMA_PARQUE = (USUARIOS [|{|moeda,passe,troco|}|]
(PARQUE ||| MAQUINA)) \ {|moeda,passe,troco|}
Figura 2.2: Exemplo de especificação CSP
2.2 CSP
11
e bilhete.a são possíveis eventos do processo CAIXA, que representa a bilheteria do
parque.
Em CSP, também é possível definir comportamentos de entrada e saída. Um processo
pode receber ou fornecer um valor. Esses são descritos através dos operadores ? (para
receber) e ! (para fornecer). Na Figura 2.2 o comportamento do processo CAIXA é
descrito inicialmente pelo recebimento do dinheiro de um cliente (dinheiro?clt), em
seguida tem duas ações de saída (bilhete!clt e troco!clt).
Além dos conceitos apresentados anteriormente, CSPM contém alguns operadores.
Esses operadores são considerados padrão para as ferramentas existentes e são utilizados para relacionar eventos e processos. A tabela 2.1 apresenta alguns operadores da
linguagem. Os outros operadores serão omitidos por não fazerem parte do escopo desse
trabalho.
STOP
SKIP
a -> Processo
Processo [] Processo
Processo |˜| Processo
Processo ; Processo
if <condiçao> then Processo else Processo
<condicão> & Processo
Processo ||| Processo
Processo [| cs |] Processo
Processo \ <cs>
Processo [[ <lista_renomeação> ]]
deadlock
finalização com sucesso
prefixação
Escolha externa
Escolha interna
composição sequencial de processos
escolha condicional
processo guardado
Intercalação de processos
Paralelismo
ocultação de canais
renomeação
Tabela 2.1: Operadores da linguagem CSP
Iniciamos apresentando os processos primitivos da linguagem, que têm comportamento básico, como o STOP que não faz nada (representa o deadlock) e o SKIP que
representa terminação com sucesso.
O prefixo é o operador mais básico da linguagem: a -> P denota um processo que
inicialmente comunica o evento a e comporta-se como P após esta comunicação. Podemos ilustrar esse operador através do processo CAIXA (Fig. 2.2), ele inicialmente oferece o evento dinheiro?clt. Após esta comunicação, o processo oferece os eventos
bilhete.clt e troco.clt, nesta ordem, voltando novamente a seu estado inicial
após ambas as comunicações ocorrerem.
Em CSP existem dois tipos de escolha, a escolha externa e a escolha interna, denotados
pelos operadores [] e |˜|, respectivamente. A escolha externa é determinada pela
ação do ambiente, ou seja, o ambiente tem controle sobre as escolhas das opções de
comportamento. Já a escolha interna tem o comportamento não determinístico, pois esse
é realizado pelo processo, sem a interferência do ambiente.
2.2 CSP
12
Na especificação (Fig. 2.2), o processo USUARIO decide internamente (|˜|) se inicialmente o cliente entra, ou só depois que efetuar pagamento. No mesmo processo existe
uma escolha externa ([]), onde o processo decide, de forma perceptível ao ambiente, se
emite primeiramente o bilhete seguido do troco ou vice-versa, .
O operador de composição (;) combina dois processos: P;Q de tal forma que executa
inicialmente o processo P e caso esse termine com sucesso, Q é executado. Podemos
observar esse comportamento no processo USUARIO, que independente das escolhas, ao
finalizá-lo, realiza sequencialmente as ações de brincar e sair levando ao estado inicial
de USUARIO.
As escolhas condicionais são recursos da linguagem CSP para determinar o fluxo
de um processo através de expressões lógicas.
Na especificação (Fig.
2.2) a esco-
lha condicional é usada no processo ENTRADA_PARQUE, onde a expressão if x ==
8 then SISTEMA_PARQUE else ENTRADA_PARQUE representa um comportamento
onde, caso a condição x == 8 seja atendida, o processo SISTEMA_PARQUE é executado,
senão ele volta a seu estado inicial (ENTRADA_PARQUE). Essa condicional se assemelha às
das linguagens de programação. Podemos também definir uma condicional através da condição de processo guardado, onde o comportamento (x == 8) & SISTEMA_PARQUE
define que PARQUE é executado se a condição x == 8 for verdadeira, caso contrário, o
processo é bloqueado.
Na composição em interleave, dois processos P ||| Q não se comunicam entre si,
apenas com o ambiente. O processo USUARIOS (Fig. 2.2) é descrito através de uma
composição entrelaçada (do Inglês, interleaving) entre de três clientes (USUARIO(a)
||| USUARIO(b) ||| USUARIO(c)), onde cada um é executado independentemente
do outro.
A expressão P [| cs |] Q denota um paralelismo, tal que P e Q são processos e
cs é o conjunto de canais de sincronização. Na especificação da Figura 2.2 encontramos
o uso desse operador no processo SISTEMA_PARQUE. O processo executa paralelamente
USUARIOS e CAIXA, que se comunicam através da sincronização nos seguintes eventos:
dinheiro, bilhete, troco. Além disso, essas ações são escondidas do ambiente
utilizando-se do operador de abstração (\). A ocultação de canais é descrita através
da expressão P \ cs, tal que o processo se comporta como P, exceto que os eventos
no conjunto cs não são visíveis pelo ambiente externo ao processo. Nesse contexto, os
eventos visíveis do processo SISTEMA_PARQUE são apenas entrar, brincar e sair.
O operador de renomeação P[[a <- b]] comporta-se como P , exceto que a
2.2 CSP
13
ocorrência do evento a será substituída pelo evento b.
quando se fala em reuso.
A renomeação é essencial
Através deste operador é possível obter novos processos
apenas renomeando seus eventos, ou seja, pode-se reaproveitar descrições específicas
do comportamento de um processo sem a necessidade de reescrevê-lo. Como exemplo, podemos citar o comportamento do processo CAIXA (Fig.
2.2) que é descrito
como o seguinte: dinheiro?clt -> bilhete!clt -> troco!clt -> CAIXA.
Caso desejemos reaproveitar esse processo para criar uma máquina com comportamento similar, mas que trabalhe em um conjunto de canais diferente, podemos utilizar o operador de renomeação. Por exemplo, MAQUINA é representado da seguinte
forma: MAQUINA = CAIXA [[dinheiro <- moeda, bilhete <- passe]], recebe o comportamento de CAIXA e a seta <- representa a renomeação do canal da esquerda pelo da direita.
Em FDR2 [BROWNLEE, 2000], podemos também fazer uso de uma linguagem funcional que possui diversas funções sobre conjuntos, sequências, tuplas, assim como casamento
de padrões. Por exemplo, union, inter e diff representam as operações de união,
interseção e diferença entre conjuntos, respectivamente. O member(x, cs) verifica se
o evento x faz parte do conjunto de eventos cs. Por exemplo, podemos verificar se o
evento brincar faz parte do conjunto de eventos J = {entrar, brincar, sair}
analisando se member(brincar, J). Finalizando, extension(c) retorna o conjunto
de valores que ”completam” o canal c. Por exemplo, na especificação da figura 2.2, são
extension(dinheiro) os valores a, b e c.
Como as interfaces são usualmente definidas em termos de canais, uma notação que
especial é fornecida para a escrita do conjunto de eventos de um canal. A notação {|c|}
expande o conjunto de eventos a partir de c, ou seja, todas as possíveis comunicações ao
longo do canal c. Por exemplo, o conjunto de eventos do canal entrada é descrito como
o seguinte: {|entrada|} = {entrada.1,entrada.2,...,entrada.10}.
A seguir apresentaremos a descrição dos modelos semânticos da linguagem CSP.
2.2.1
Semântica CSP
Na literatura podemos encontrar três modelos semânticos para CSP: operacional,
algébrica e denotacional [ROSCOE ET al., 1997]. Na semântica operacional, o processo é
um sistema em transição (ou máquina de estados), e a ocorrência de um evento representa
uma transição. Na semântica algébrica, as propriedades do processo podem ser deduzidas
por transformações sintáticas, seguindo um conjunto de leis algébricas. Na semântica
2.2 CSP
14
denotacional, CSP pode ser interpretada em três níveis: modelo de traces, falhas e falhadivergência [SCHNEIDER, 1999], que serão apresentadas a seguir.
Modelo de traces
Um aspecto importante do comportamento de um processo está relacionado a ocorrência dos eventos na ordem de seus acontecimentos. No modelo de traces, o processo
é descrito através (do conjunto) das possíveis sequências de eventos que ele pode vir a
executar. O conjunto de todos os possíveis traces de um processo P é chamado traces(P )
e define a semântica de um processo.
Um trace pode ser representado explicitamente pela ordem da listagem de
seus elementos.
Para entendermos melhor, vamos considerar o seguinte processo:
PARQUE = entrar -> brincar -> sair -> SKIP. Podemos extrair as seguintes sequências em cada execução de PARQUE:
entrar -> brincar -> sair -> SKIP
↓entrar
→ hentrari
brincar -> sair -> SKIP
↓brincar
→ hentrar, brincari
sair -> SKIP
↓sair
→ hentrar, brincar, sairi
SKIP
↓√
→ hentrar, brincar, sair, ticki
Como podemos observar, cada sequência de ações realizada por um processo representa
um trace, tal que, por exemplo, hai descreve uma sequência de execuções do processo e
ha, bi consiste nos eventos a seguido por b, que descreve outra sequência. Logo, levando-se
em consideração que a sequência vazia hi sempre fará parte do conjunto de traces do
processo, os traces de PARQUE são representados como:
traces(P ARQU E) = {hi, hentrari, hentrar, brincari, hentrar, brincar, sairi,
hentrar, brincar, sair, ticki}
O processo PARQUE poderia ter um conjunto infinito de traces caso ele fosse recursivo:
PARQUE = entrar -> brincar -> sair -> PARQUE. Neste caso, seu modelo de
traces será representado da seguinte forma:
traces(P ARQU E) = {hi, hentrari, hentrar, brincari, hentrar, brincar, sairi,
hentrar, brincar, sair, entrari...}
2.2 CSP
15
e seu comportamento sempre leva ao estado inicial. Porém, seu espaço de estados é
finito, ou seja, o processo executa infinitamente, mas cada ação do seu comportamento é
executada finitamente. como descrito na Figura 2.3.
Figura 2.3: Máquina de estado do processo PARQUE criada pelo FDR2
Por se tratar de uma sequência, diversas operações podem ser utilizadas para compor
traces. A operação de concatenação é uma delas, onde seq1 ˆseq2 representa a sequência
de elementos de seq1 seguida pelos de seq2 . Com esse operador é possível gerar um novo
trace através da junção de outros dois. Por exemplo, no processo PARQUE a concatenação
dos traces hentrar, brincar, sairi ˆ hentrari gera o trace hentrar, brincar, sair, entrari.
A operação #seq define o tamanho de uma sequência, retornando o número de
elementos contidos nela.
Por exemplo, #hentrar, bricar, sairi = 3.
A projeção de
uma sequência seq sobre os elementos de um conjunto A (seq A) representa uma
subsequência de todos os elementos de seq que estão nesse conjunto. Por exemplo,
hentrar, brincar, sair, entrari {entrar, brincar} = hentrar, brincar, entrari.
Se seq é uma sequência não vazia, ela pode ser descrita como hs0 i ˆs1 , onde
s0 é o primeiro elemento e s1 é o resto da sequência.
Nesse contexto, duas fun-
ções são definidas: head(seq) = s0 e tail(seq) = s1 . Por exemplo, para a sequência
hentrar, brincar, sair, entrari : s0 = entrar e s1 = hbrincar, sair, entrari.
A semântica de traces de um processo CSP é descrita através de um conjunto de regras,
as quais são descritas de acordo com os operadores da linguagem. A seguir apresentaremos
algumas delas:
√
traces(SKIP ) = {hi, h i}
traces(ST OP ) = {hi}
traces(a → P ) = {hi} ∪ {hai ˆtr | tr ∈ traces(P )}
traces(P []Q) = traces(P ) ∪ traces(Q)
traces(P |˜| Q) = traces(P ) ∪ traces(Q)
Como podemos observar nas regras descritas acima, os operadores de escolha externa
2.2 CSP
16
([]) e interna (|˜|) possuem os mesmos conjuntos de traces, pois este modelo preocupa-se
apenas com a sequência de eventos que um processo pode executar, definindo uma visão
apropriada para as propriedades de segurança. No entanto, não é possível definir com
esse modelo onde os processos podem falhar.
Para tal, a fim de diferenciar o não-determinismo, é preciso estender o modelo de
traces com informações adicionais, o que é feito pelo modelo que apresentamos a seguir.
Modelo de falhas
O modelo de falhas descreve o que um processo pode fazer e quais conjuntos de eventos
podem ser recusados ao executar cada ação do processo, ou seja, esse modelo determina
quais eventos podem não ser aceitos pelo processo após uma ação dele. Essa falha é
definida através do par (t, X), tal que t ∈ traces(P ) e X representa todos os valores que
podem ser recusados por P após a execução de t. Com isso, o conjunto de todas as
possíveis falhas de P é chamado de f ailures(P ).
Esse modelo permite verificar se um processo é determinístico ou não, o que não é
possível no modelo de traces. Um processo é dito determinístico se toda vez que seu comportamento é observado a partir de um estado conhecido/determinado (mesma entrada),
o resultado é sempre o mesmo.
Para
tes
exemplificar
processos:
o
modelo
de
falhas,
vamos
considerar
os
seguin-
PORTAO1 = entrar -> STOP [] sair -> STOP
PORTAO2 = entrar -> STOP |˜| sair -> STOP.
e
Os processos PORTAO1
e PORTAO2 possuem os mesmos traces, porém não são semanticamente equivalentes,
considerando os conjuntos de eventos que podem não ser aceitos em cada transição. A
Figura 2.4 ilustra o gráfico de transição desses processos no modelo de falha.
Figura 2.4: Processos PORTAO1 e PORTAO2 com seus estados e suas recusas
2.2 CSP
17
Observando a transição de estados do PORTAO1, ao executar qualquer ação, o processo
recusa ambos eventos. Por exemplo, para as duas opções que o processo tem, caso ele
execute entrar, depois dessa ação, ele pode recusar entrar e sair. Já o processo
PORTAO2, devido a escolha interna (representada pelo símbolo τ ), possui uma transição
que permite executar um evento e recusar o outro.
Essa abordagem é válida para processos que não divergem. Quando há necessidade
de analisar esse comportamento, devemos usar o modelo a seguir.
Modelo de falha-divergência
O modelo de falhas/divergência tem sido considerado padrão para CSP, pois inclui os
dois modelos anteriores. Este permite investigar o que um processo pode fazer, identificar
suas falhas e verificar suas divergências.
A divergência é um dos piores comportamentos que um componente do sistema pode
apresentar, levando-se em consideração que outros componentes podem ficar na espera,
consumindo recursos computacionais, enquanto aguardam que em algum momento o processo consiga sincronizar [SCHNEIDER, 1999].
Quando um processo realiza uma sequência infinita de eventos internos, não há garantias de que em algum momento o processo vai alcançar um estado estável. A Figura 2.5
ilustra o exemplo de dois processos divergentes.
Figura 2.5: Processos divergentes
Os
processos
e
PORTAO3 = entrar -> PORTAO3
PORTAO4 = entrar -> PORTAO4 [] sair -> STOP
através das maquinas de estado da seguinte forma:
que
são
representados
PORTAO3 \ {entrar}
e
PORTAO4 \ {entrar} , têm execuções divergentes, devido à ocultação de seus
canais.
Na modelagem de falha e divergência, o conjunto de falhas é estendido para
capturar a ideia de um processo poder falhar após ter divergido.
Sua se-
mântica é definida para cada processo pelo par (f ailures⊥ (P ), divergences(P )),
onde divergences(P ) é o conjunto de traces s em que P pode divergir, e
2.2 CSP
18
f ailures⊥ (P ) = f ailures(P ) ∪ {(s, X)|s ∈ divergences(P )}, ou seja, o conjunto de falhas
do processo após divergir. Esse comportamento é diferente das f ailures(P ), que representa o conjunto de falhas do processo após a execução de cada trace.
Refinamento
Refinar um sistema significa criar uma nova modelagem ou implementação (sair do
abstrato para algo mais próximo da implementação) de modo que o comportamento seja
compatível. Em CSP, todos os três modelos semânticos apresentados anteriormente (traces, falhas e falhas-divergência) possuem suas formas de refinamento que são possíveis
verificar através da ferramenta FDR2.
O modelo de traces está relacionado a sequência de eventos que um processo pode
executar. Nesse modelo, um processo P é refinado por um processo Q (P vT Q) se todas
as possíveis sequências de eventos de Q são possíveis em P (traces(Q) ⊆ traces(P )).
O modelo de falhas indica o que um processo pode recusar após a execução de um
trace. Nesse modelo, um processo P é refinado por um processo Q (P vF Q) se Q não
introduz nenhuma falha quando substitui P , além de não introduzir nova sequência de
comunicação traces(Q) ⊆ traces(P ) e f ailures(Q) ⊆ f ailures(P ).
O modelo de falhas e divergências é o único capaz de investigar se o processo refinado não introduz mais divergências.
Um processo P
é refinado
por Q se as possíveis sequências em que Q diverge e seu conjunto de falhas
ao divergir, são possíveis em P .
Seu refinamento é definido como seguinte:
P vF D Q ≡ f ailures(Q)⊥ ⊆ f ailures(P )⊥ ∧ divergences(Q) ⊆ divergences(P ).
Baseado nesses modelos semânticos, foram implementadas diversas ferramentas de
suporte a CSP. A seguir, apresentaremos algumas delas.
2.2.2
Ferramentas para CSP
CSP possui algumas ferramentas que auxiliam tanto no processo de modelagem e
verificação, como na visualização gráfica do comportamento dos processos. A seguir apresentamos quatro dessas ferramentas: FDR2, ProBE, ProB e TypeChecker.
FDR2
O FDR2 (Failures-Divergence Refinement) [BROWNLEE, 2000] é uma ferramenta que
se fundamenta na teoria de concorrência e realiza verificações para os modelos semânticos
de especificações CSP.
2.2 CSP
19
Sendo um produto da Formal System 1 , FDR2 foi a primeira ferramenta comercial
disponível para CSP e desempenhou um papel importante na sua evolução. O FDR2 está
disponível para as plataformas Linux, Solaris e Mac OS.
Usando FDR2, é possível verificar refinamento de processos nos três modelos descritos
anteriormente. Além disso, é possível a utilização do FDR2 sem interface gráfica. Em
nosso trabalho, usamos a interface ’batch’ para executar as asserções do script gerado pela
BTS. Essas asserções são usadas para afirmar propriedades e refinamento, e são definidas
da seguinte forma:
assert Abstract [X= Concrete
onde Abstract e Concrete são processos e o X indica o tipo de comparação: T para
traces, F para falhas e FD para falha e divergência.
FDR2 também permite a verificação de várias condições de exatidão, como ausência
de deadlocks e livelocks, podendo ser investigado os motivos quando essas não são satisfeitas, e nos auxilia na verificação de comportamentos determinísticos para os modelos
apresentados anteriormente. A seguir, temos alguns exemplos de asserções que podem ser
aplicadas na especificação da Figura 2.2.
assert PARQUE :[ deterministic [FD] ]
assert USUARIOS :[ deadlock free [F] ]
assert SISTEMA_PARQUE :[ divergence free ]
assert SISTEMA_PARQUE [T= PARQUE
Como podemos observar, além da verificação de refinamento, o FDR2 também permite
avaliar diretamente se um processo é determinístico, livre de deadlocks e divergência.
Na Figura 2.6 podemos visualizar a interface da ferramenta FDR2, bem como a ilustração da verificação dessas asserções na parte central. O resultado da verificação dessas
√
asserções, válido ou não, é representado por um
verde e um χ vermelho, respectivamente.
Uma característica importante do FDR2 são os contraexemplos. Quando uma asserção
é selecionada para depuração, é criada uma nova janela com informações de contraexemplos que foram encontrados (caso haja) enquanto a asserção era analisada. Sendo possível
explorar as razões das asserções falsas.
1 http://www.fsel.com/software.html
2.2 CSP
20
Figura 2.6: Interface da FDR2
ProBe
ProBe [PROBE. . . , 2003] é um animador para CSP que permite ao usuário explorar
o comportamento dos modelos interativamente. A ferramenta exibe uma lista com as
possíveis ações e estados que um processo pode executar. Assim o usuário pode verificar
um dado comportamento do processo e detectar problemas.
O ProBe é gratuito e possui versões para Windows, Linux, FreeBSD e Solaris. Além
de ser muito simples de usar, é notável sua importância para o ensino de CSP, pois é
possível visualizar o comportamento dos processos de forma interativa, como podemos
observar na Figura 2.7.
Figura 2.7: Interface da ProBe
2.2 CSP
21
ProB
Assim como o ProBe, o ProB 2 (Fig. 2.8) é outro animador e model-checker [CLARKE
JR. et al., 1999] que oferece suporte a CSP e outras linguagens formais, como método B
[SCHNEIDER, 2001], Z [SMITH, 2000], Event-B [ABRIAL et al., 2010] e TLA [LAMPORT, 1994]. Esta permite que as especificações sejam verificadas de forma automática
e animada, ajudando na detecção de erros.
ProB é gratuito e possui versões Windows, Linux e OS X.
Figura 2.8: Interface da ProB
Na Figura 2.8 podemos visualizar, na parte superior, uma especificação CSP e na parte
inferior central é possível explorarmos o comportamento dos processos CSP, clicando sobre
eles.
TypeChecker
TypeChecker é um verificador de tipos da linguagem CSP, ou seja, ele é utilizado basicamente para verificar se a especificação foi definida corretamente, no tempo de tradução
do programa (ou tempo de compilação). O TypeChecker não possui interface gráfica e é
executado através de linhas de comando.
Em nossa ferramenta utilizamos o verificador de tipo para analisar os comportamentos
2 http://www.stups.uni-duesseldorf.de/ProB/index.php5/Main_Page
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
22
externos, descritos pelo usuário.
2.3
Abordagem para o desenvolvimento sistemático e
confiável de sistemas baseados em componentes
O trabalho desenvolvido em [RAMOS, 2011] apresenta uma abordagem que propõe
a composição sistemática e segura de componentes. Essa descreve um modelo de componente que se concentra em seus conectores e impõe restrições necessárias para uma
interação segura. A estratégia define quatro regras de composição: interleave, communication, feedback e reflexive. Estas asseguram corretude na composição, como a ausência
de deadlocks.
Iniciaremos a apresentação da abordagem descrevendo o modelo de componente proposto.
Modelo de componente
Um contrato descreve o comportamento que um componente deve ter para obter confiança. Nesse sentido, [RAMOS, 2011] definiu um modelo de componente que representa
o componente, seus conectores e sua interação semântica, formando a base para uma
composição segura.
Na abordagem, componentes e conectores (Figura 2.9) são representados basicamente
por elementos caixa-preta, descritos através de um processo CSP, com seus canais e tipos
específicos, que definem um comportamento externo, seus pontos de interação (ou portas)
e suas interfaces, respectivamente.
Figura 2.9: Modelo de componente
Para ilustrar melhor, vamos considerar um exemplo clássico de um cliente-servidor
(Figura 2.10). O exemplo consiste em um sistema de caixa eletrônico, onde o Cliente e a
Maquina representam componentes no sistema.
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
23
Figura 2.10: Exemplo de um Cliente-Servidor
Utilizaremos esse exemplo durante toda essa seção para apresentar as regras e propriedades da abordagem. O comportamento dos componentes, bem como seus tipos e canais
são descritos a seguir.
NUM = {0..20}
datatype DADOSMQ = rt.NUM | requisitaSaldo | ackRt.Bool | recSaldo.NUM
datatype DADOSCL = insereCartao.NUM | digitaSenha.NUM | retiraDin.NUM |
saldo | retiraCartao | recebeDin | mostraSaldo
channel cl : DADOSCL
channel maq : DADOSMQ
Figura 2.11: Descrição dos tipos e canais
Cliente = cl.insereCartao?num -> cl.digitaSenha?num ->
(SAQUE [] SALDO) ; cl!retiraCartao -> Cliente
SAQUE = cl.retiraDin? val -> maq.rt.val ->
maq.ackRt?a -> cl!recebeDin -> SKIP
SALDO = cl.saldo -> maq.requisitaSaldo ->
maq.recSaldo?x -> cl!mostraSaldo -> SKIP
Figura 2.12: Descrição do comportamento do componente Cliente
Maquina =
|~| a: Bool @ maq.rt?x -> maq.ackRt.a -> Maquina
[]
|~| y: NUM @ maq.requisitaSaldo -> maq!recSaldo.y -> Maquina
Figura 2.13: Descrição do comportamento do componente Máquina
A especificação inicialmente apresenta os tipos e canais (Fig. 2.11) utilizados pelos
componentes. Em seguida, temos o comportamento de Cliente (Fig. 2.12) e Maquina (Fig.
2.13). O processo Cliente recebe do usuário, através do canal cl, o número do cartão
seguido da senha. Logo após, é oferecida um escolha entre sacar dinheiro (SAQUE) e
verificar saldo (SALDO). Já o processo Maquina tem o comportamento de retirar dinheiro
ou verificar saldo, de acordo com a escolha do Cliente. Por exemplo, maq.retirar.val
representa um valor de saída que vai ser recebido em maq.retirar?x no processo Maquina.
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
24
Nesse processo existe uma escolha externa entre retirar dinheiro ou requisitar saldo. O
operador @ representa uma separação entre o valor que está sendo recebido internamente
e a execução dos eventos.
Como podemos observar, o comportamento do componente está relacionado à ação
de interação, não se preocupando com o que ocorre internamente. Ou seja, relaciona-se
com o que ele pode receber e fornecer para outro componente. Por isso as ações de seu
comportamento são externas.
Nesse contexto, a interface de comunicação do componente é representada por dois
conjuntos de eventos CSP: eventos de entrada e eventos de saída, onde os valores de saída
de um componente são recebidos na entrada de outro e essa comunicação pode representar
um par request-response. O comportamento da comunicação entre dois componentes
(representado pelo elemento central da Fig. 2.10 (CON )) será explicado mais a frente. A
seguir apresentaremos a definição do modelo de componente.
Definição 1 (Contrato de Componente). U m contrato de componente Ctr : hB, R, I, Ci
é descrito através de um comportamento B, um conjunto de canais (portas) de
comunicação C, um conjunto de interf aces I e uma f unção total entre canais e
interf aces R : C → I, tal que :
• B é um processo de entrada e saída (I/O P rocess).
• R representa a relação entre canais e o conjunto de tipos, cujo dom(R) = C ∧
img(R) = I.
• Os eventos de todos os seus canais C devem estar associados a dois conjuntos disjuntos: inputs e outputs.
O comportamento desses componentes é representado por um I/O P rocess (processo
de entrada e saída), que em CSP é definido por um processo P que deve satisfazer a cinco
condições:
1. Canais de entrada e saída: Os eventos de um canal fazem parte das ações de entrada
ou saída de um processo. Por exemplo, no sistema Cliente-servidor as entradas e
saídas para o Cliente são definidas através das funções inputs e outputs, como o
seguinte:
inputs(maq, Cliente) = { maq.ack, maq.recSaldo}
outputs(maq, Cliente) = { maq.retirar, maq.requisitaSaldo}
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
25
onde a interseção de inputs e outputs é vazia e a sua união é subconjunto de {|maq|}.
Como podemos observar, o processo Cliente satisfaz essa condição, pois não possui
eventos em comum nas entradas e saídas.
2. Traces infinitos: P deve ter traces infinitos (mas espaço de estado finito).
3. Ausência de divergência: P é livre de divergência.
4. Entrada Determinística: Se um conjunto de eventos de entrada em P é oferecido
pelo ambiente, nenhum desses pode ser recusado. Esse determinismo é muito importante, pois o processo nunca vai recusar um serviço oferecido por outro processo
(componente). Essa condição é baseada na semântica de falhas que garante que se
P executa um trace s ˆ hc.ai, tal que hc.ai é uma entrada, então esse evento não
pode ser recusado por P após s ((s, {c.a}) ∈
/ f ailures(P )).
Nos processos Cliente e servidor essa propriedade é satisfeita, visto que não há
escolha interna entre os eventos de entrada.
5. Saída Fortemente Decisiva: todas as escolhas entre eventos de saída de um determinado canal em P são internas. Essas decisões são baseadas nas ações de entrada do
processo, o que gera um não determinismo na saída. Na saída decisiva, dado o trace
s ˆ hc.bi tal que c.b pertence à saída de P , toda saída em c será recusada, exceto c.b
- representado por (s, outputs(c) \ hc.bi) ∈ f ailures(P ). Com isso, é notável que o
processo sempre irá oferecer uma saída nesse canal.
Os processos Cliente e servidor satisfazem essa condição, pois não há escolha nas
suas saídas e quando essa é oferecida, existe apenas uma opção de saída.
Os comportamentos de Entrada Determinística e Saída Decisiva são propriedades que
indicam como um componente deve aceitar e enviar informações.
Esse modelo de componente é chamado de BRIC (Behavior, relation, interfaces, channels) e descreve as condições que devem ser atendidas para se obter um componente confiável. No sistema Cliente-servidor (Fig. 2.10), o contrato de componente de Cliente e
Maquina são definidos como o seguinte:
CtrCliente = hCliente, {cl 7→ DADOSCL, maq 7→ DADOSM Q}, {DADOSCL, DADOSM Q}, {cl, maq}i
CtrM aquina = hM aquina, {maq 7→ DADOSM Q}, {DADOSM Q}, {maq}i
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
26
Como podemos observar, as definições descritas até agora observam o componente
e seu comportamento. Essas características são fundamentais para que as propriedades
e restrições dos componentes sejam garantidas e a aplicação das regras de composição
tenham o resultado desejado. Por isso, uma das principais características da abordagem proposta em [RAMOS, 2011] é resolver os problemas esperados antes de integrar os
componentes.
Descreveremos a seguir algumas propriedades importantes relacionadas a verificação
da interação segura desses componentes.
Protocolos de comunicação
Outra importante característica do componente é o protocolo de comunicação. Esse
está relacionado a interação de um componente com outro no sistema.
Os protocolos são importantes para realizar verificações mais específicas sobre a interação dos componentes, analisando a comunicação através de um canal. A seguir apresentaremos algumas características do protocolo de comunicação.
• Implementação:
cesso
P
é
A implementação do protocolo de um canal ch do pro-
descrita
como
todo
comportamento
do
processo
sobre
ch
(P rotIM P (P, ch) ≡F P {ch}), tal que P rotIM P deve ter os mesmos traces e falhas do processo sobre a projeção desse canal. Ou seja, os traces e falhas desses
devem ser equivalentes (≡F ). A projeção é toda execução de ch em P .
No exemplo do Cliente-servidor o canal maq representa a interação de cada componente. Existe o protocolo a partir do ponto de vista do Cliente e da Maquina.
Estes são definidos a partir do comportamento do processo. Por exemplo, definido
o comportamento do componente Cliente, seu protocolo representa todo comportamento de Cliente no canal maq, como descrito na Figura 2.14. Da mesma forma,
para a Maquina, seu protocolo é representado por todo comportamento do processo
Maquina sobre o canal maq, como descrito na Figura 2.15.
Prot_Cliente =
|~|x: NUM @ maq!rt.x -> maq.ackRt?a -> Prot_Cliente
[]
maq.requisitaSaldo -> maq.recSaldo?x -> Prot_Cliente
Figura 2.14: Protocolo do Cliente para o canal maq
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
27
Prot_Maquina =
|~| a: Bool @ maq.rt?x -> maq.ackRt.a -> Prot_Maquina
[]
|~|x: NUM @ maq.requisitaSaldo -> maq!recSaldo.x -> Prot_Maquina
Figura 2.15: Protocolo da Maquina para o canal maq
Os protocolos de comunicação descritos na Figura 2.14 e 2.15 são referentes a todas as ações do canal de interação maq, tanto para o componente Cliente como a
Maquina.
Nesse exemplo, não é implementado protocolo de comunicação para o canal cl, pois
este não interage com nenhum componente. Se quisermos tratar o ambiente (usuário) que utiliza esse serviço como outro componente, consequentemente teremos uma
interação deste com o componente Cliente.
• Satisfação: Um protocolo é válido quando ele satisfaz o seguinte refinamento: (Q vF
P rotIM P (P, ch)), onde Q corresponde a um protocolo que deve ser refinado pela
comunicação do processo P sobre o canal ch.
No exemplo do Cliente-Servidor, para analisar se o protocolo Prot_Cliente satisfaz
o processo Cliente é necessário realizar uma verificação através do refinamento CSP,
ou seja, verificar se o conjunto de traces e falhas da projeção de Cliente sobre o
canal maq refina Prot_Cliente (P rot_Cliente vF P rotIM P (Cliente, maq)).
Esses protocolos de comunicação são descritos para analisar a relação entre a comunicação de dois processos, focando unicamente em seus protocolos. Verificar a compatibilidade desses é uma forma de garantir que a comunicação entre dois processos, que são
I/O processes, é livre de deadlocks. A propriedade de compatibilidade de protocolo é
descrita a seguir.
• Protocolos fortemente Compatíveis: a saída de um processo sempre será aceita
pelo outro processo. Esse tipo de verificação é de extrema importância para o sistema, pois consegue garantir que nenhuma informação gerada (saída) pelo componente será perdida.
Analisar a compatibilidade entre dois protocolos através de refinamento CSP pode ser
definido através do processo chamado dual protocol [VALLECILLO et al., 2006]. O dual
de um protocolo Q é definido como um processo do qual seu conjunto de entrada e saída
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
28
é igual as outputs(Q) e inputs(Q), respectivamente, e que tem os mesmos conjuntos de
traces, ou seja, os eventos de entrada de Q correspondem a saída de seu dual e os eventos
de saída de Q são correspondidos na entrada de seu dual.
Nesse contexto, podemos definir o dual protocol do Prot_Cliente como descrito na
Figura 2.16.
DUAL_Prot_Cliente =
|~|a: Bool @ maq.rt?x -> maq.ackRt.a -> DUAL_Prot_Cliente
[]
|~|x: NUM @ maq.requisitaSaldo -> maq.recSaldo!x -> DUAL_Prot_Cliente
Figura 2.16: Dual-protocol de Prot_Cliente
Para ser compatível, o DUAL_Prot_Cliente deve ser refinado pelo protocolo do outro
componente, em nosso exemplo, Prot_Maquina, cuja condição é satisfeita.
Instância de Componente
Uma das vantagens do desenvolvimento baseado em componente é a reutilização.
Normalmente um componente é definido uma vez e reusado múltiplas vezes, e em vários
contextos diferentes. Nessa abordagem, o contexto é representado por um conjunto de
canais (que representam os pontos de interação) e é usado para comunicar um único
componente no ambiente. Nesse sentido, a substituição dos canais de um componente
por outros, significa que ele supostamente poderá interagir com outro ambiente. Essa
substituição é representada pela renomeação de um conjunto de canais de um componente
em novos. Nesse contexto, a reutilização é feita através da atribuição de nova identificação
ao componente que se deseja usar.
Figura 2.17: Reutilização de componente
A Figura 2.17 apresenta esse processo, onde é definido um novo contrato de componente cujo nome e canais são derivados da renomeação do anterior. O comportamento
do novo componente é o mesmo, exceto que ele utiliza um novo conjunto de pontos de
interação. Esse novo componente é descrito como uma instância do anterior.
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
29
Maquina1 = Maquina [[ maq <- maq_1 ]]
Figura 2.18: Criando um novo componente Máquina
No exemplo do Cliente-servidor, uma instância do componente Maquina pode ser definido como na Figura 2.18, onde o componente Maquina1 possui o mesmo comportamento
de Maquina, porém, com seu nome e canal renomeado.
A instância de componente é útil quando desejamos construir sistemas cujos componentes possuem características idênticas.
Composição
Nessa abordagem, a comunicação entre componentes é assíncrona. Para representar
essa comunicação um buffer é apresentado como elemento intermediário da composição
(Figura 2.19). Ele copia as informações de um canal para outro, ignorando se o outro
componente está ativo para receber entradas.
Apresentaremos a seguir como a comunicação assíncrona dos processos que são I/O
P rocess é especificada via buffer.
A definição de buffer em CSP é descrita como um processo com dois canais, sendo
um de entrada e um de saída, onde eles possuem o mesmo tipo. O buffer copia as
informações do seu canal de entrada para o seu canal de saída de modo que nenhuma
produção é perdida.
Figura 2.19: Exemplo de comunicação via Buffer
Na abordagem de [RAMOS, 2011], o mapeamento entre entrada e saída é traduzida
como uma renomeação entre as interfaces. Considerando isso, foi definida uma função
BU F FIO que recebe um par de canais e renomeia a interface de entrada pela interface
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
30
a→b = {a.x 7→ b.x}, tal que
de saída. A renomeação usada no buffer é descrita como: RIO
a→b substitui saídas em a por
x é uma extensions(a) e a.x ∈ outputs. Desta forma, RIO
entradas correspondentes em b.
Para sistemas modelados por meio de máquinas de estado e especificados via buffer,
existem duas propriedades que permitem o mecanismo de verificação, sem explosão dos
estados:
• Entrada e Saída Confluente: Se um processo possui ações de canais distintos a
serem executadas, uma não impede a outra de ser executada, a menos que seja no
mesmo canal.
Os processos Cliente e Maquina são I/O Confluente. Eles são o exemplo mais simples, onde não há escolha entre os eventos de diferentes canais, nem entre entradas
e saídas.
• Propriedade de Saída Finita: Como o comportamento de I/O process é livre
de divergência, a ausência de divergência ao ocultar a saída de um canal garante
que o processo sempre comunica um número finito de saídas possíveis (ou seja, o
tipo do canal é finito).
Nesse sentido, um processo Cliente, por exemplo, tem propriedade de saída finita se
para todo canal c pertencente ao conjunto de canais de Cliente, o comportamento
Cliente \ outputs(c, Cliente) é livre de divergência.
Como descrito anteriormente, a compatibilidade de protocolo é usada para verificar
a comunicação entre dois processos. Porém, é interessante verificar a relação entre diferentes canais de um mesmo componente para preservar propriedades comportamentais na
composição. Apresentaremos a seguir duas propriedades que comparam a comunicação
entre eventos de um mesmo processo.
• Canais Desacoplados: A comunicação do canal de um processo não interfere na
comunicação do outro. Na Figura 2.20, a comunicação do canal c1 é independente
de c2. Nesse contexto, os canais são desacoplados porque não introduzem nenhum
ciclo de dependência.
• Compatibilidade de Auto-Injeção com Buffer: permite a injeção de informações entre dois canais de um processo (Figura 2.21), através de buffers internos à
composição, sem introduzir deadlocks.
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
31
Figura 2.20: Canais desacoplados
Figura 2.21: Compatibilidade de Auto-Injeção com Buffer
Regras de Composição
As regras de composição introduzidas em [RAMOS, 2011] são apresentadas em uma
ordem incremental de complexidades e focam em cenários específicos de composição. As
quatro regras são interleave, communication, feedback e reflexive. Estas podem prever a
ausência de deadlocks e cada composição criam um novo componente que inclui os dois
anteriores.
A Figura 2.22 apresenta a estrutura de três dessas regras de composição. As composições em interleave e communication são binárias (comunicam canais de dois componentes).
Já as composições em feedback e reflexive são unárias, pois estão relacionadas a comunicação de diferentes canais em um mesmo componente. As regras de composição unária
têm a mesma estrutura, sendo diferenciadas apenas pelas condições impostas.
Figura 2.22: Exemplo de três regras de composição
Na composição por interleave, dois componentes, mesmo após a composição, não se
comunicam entre si, apenas com o ambiente, sem haver interferência entre eles. Para
que esse tipo de composição ocorra é necessário que os componentes não compartilhem
nenhum canal de comunicação. A definição da composição por interleave é descrita a
seguir.
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
32
Definição 2 (Composição em Interleave). Se P e Q são dois contratos de componentes,
tal que P e Q não possuem canais em comum (CP ∩ CQ = ∅, onde CP e CQ representam
o conjunto de canais dos processos P e Q, respectivamente), então, a composição em
interleave de P e Q é dada por:
P [k|]Q = Phi hi Q
O operador de composição representa uma interação assíncrona entre duas sequências de canais, mediada pela ideia de buffers infinitos. Na definição acima, a composição
não envolve comunicação, o que indica não haver qualquer tipo de interferência de um
sobre o outro. Tomando como exemplo o sistema Cliente-servidor (Fig. 2.10), para adicionarmos dois componentes Cliente no sistema, não é necessário existir comunicação entre
eles, apenas deles com a Maquina. Para isso, podemos compor esses componentes da
seguinte forma:
Cliente1 = Cliente[[cl < −cl1, maq < −maq1 ]]
Cliente2 = Cliente[[cl < −cl2, maq < −maq2 ]]
Cliente1[k|]Cliente2 = Cliente1hi hi Cliente2
onde inicialmente dois componentes Cliente são instanciados e posteriormente são colocados em interleave.
A segunda regra de composição é o caso tradicional, ou seja, caminho mais comum
para comunicar canais de diferentes componentes, como no exemplo da comunicação entre
o Cliente e a Maquina.
Definição 3 (Composição por Comunicação). Se P e Q são dois contratos de componentes
e ic e oc dois canais de comunicação, tal que
• ic ∈ CP ∧ oc ∈ CQ ,
• CP ∩ CQ = ∅
ic→oc ]] e P rot
oc→ic ]]
e os protocolos de comunicação P rotIM P (P, ic) [[RIO
IM P (Q, oc) [[RIO
• Possuem Entrada e saída confluente
• Têm Forte compatibilidade
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
33
• E satisfazem a propriedade de saída finita
A composição em comunicação de P e Q através de ic e oc é definida como o seguinte:
P [ic ↔ oc]Q = Phici hoci Q
Os componentes têm diferentes pontos de interação e sua comunicação é assíncrona.
Além disso, outras restrições devem ser aplicadas para se ter um processo livre de deadlocks, como a implementação dos protocolos dos canais que fazem parte da comunicação (P rotIM P ). Estas restrições aplicam-se a uma versão renomeada destes protocolos:
oc→ic ]] que substitui a saída de oc pela entrada de ic em P . Além disso, esses proP [[RIO
tocolos devem atender três propriedades que garantem a confiabilidade da composição.
A Entrada e saída confluente e a Forte compatibilidade permitem o mecanismo de verificação do sistema, sem explosão dos estados e a propriedade de saída finita garante a
interoperabilidade de dois componentes.
Na construção do sistema, um conjunto de componentes compostos sempre representará um único componente. Compor as saídas e entradas desse conjunto de componentes
permite introduzir ciclos na estrutura. Devido à existência desses ciclos, novas condições devem ser levadas em consideração para preservar propriedades comportamentais na
composição. Este tema está relacionado com o estudo de abordagens mais gerais para
garantir sistemas livres de deadlocks. Esse identifica que deadlocks surgem em topologias
complexas (gráficos) pela presença de ciclos indesejáveis.
A terceira regra de composição foi baseada no conceito de canais desacoplados. De
acordo com essa noção, a comunicação em um canal não interfere na comunicação do
outro (essa é intercalada).
Definição 4 (Composição em Feedback).
Se P é um contrato de componente, e
ic→oc ]] e
ic e oc dois canais de comunicação, tal que os protocolos P rotIM P (P, ic) [[RIO
oc→ic ]]
P rotIM P (P, oc) [[RIO
• Possuem Entrada e saída confluente
• Têm Forte compatibilidade
• Satisfazem a propriedade de saída finita
• {ic, oc} ⊆ CP
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
34
• ic e oc são desacoplados em P
A composição em feedback de oc em ic é definida como o seguinte:
P [oc ,→ ic] = P |
hici
hoci
Esta regra impõe algumas condições que são similares a regra de composição de comunição, exceto que adicionalmente aplica a restrição que os canais sejam desacoplados.
A última regra de composição é mais geral que o feedback. Essa é para topologias
mais complexas, onde são verificados problemas de dependência sobre a comunicação dos
eventos no sistema.
Definição 5 (Composição Reflexiva). Se P é um contrato de componente, e ic e oc dois
canais de comunicação, tal que
• {ic, oc} ⊆ CP
• P {| ic, oc |} satisfaz uma propriedade de saída finita.
• E P {|ic, oc|} é Compatibilidade de Auto-Injeção com Buffer
Assim, a composição reflexiva de P de oc em ic é definida como o seguinte:
¯ ic] = P |
P [oc ,→
hici
hoci
Considerações Finais
A abordagem de [RAMOS, 2011] apresenta características de grande importância
para verificação da composição entre componentes. Porém, o mercado de software busca
automação dos processos. Assim sendo, a aplicação de métodos, como o proposto em
RAMOS, na prática exigem ferramentas que facilitem sua utilização, auxiliando o usuário
e trazendo agilidade ao desenvolvimento.
Esta dissertação tem como principal objetivo o desenvolvimento e validação de uma
ferramenta que consiga prever a composição entre componentes utilizando todo conjunto
de propriedades e regras proposto nesse capítulo.
2.3 Abordagem para o desenvolvimento sistemático de sistemas confiáveis
35
Buscamos o máximo de automação possível, reduzindo a complexidade através da
ocultação dessas regras e propriedades. Além disso, com a finalidade de facilitar a usabilidade do usuário, buscamos o mínimo de dificuldade através da descrição de uma interface
amigável.
Para entendermos como funcionará a ocultação de todas as regras e propriedades
apresentadas nesse capítulo, o próximo capítulo apresenta o trabalho proposto em [OLIVEIRA, 2012b] que descreve a implementação dessas, aplicadas a um estudo de caso,
através de asserções FDR2.
36
3
Uma verificação formal para
desenvolvimento de sistemas confiáveis
baseados em componentes
No capítulo anterior conhecemos o trabalho descrito em [RAMOS, 2011] que propõe
a composição sistemática e confiável de componentes. Nele, algumas condições foram
expressas em termos de refinamentos que podem ser verificados automaticamente em
FDR2. No entanto, muitas das condições foram descritas diretamente na semântica de
CSP. A prova destas condições requer uma interação com provadores de teoremas que
dificultariam a aplicação prática dessa estratégia. Nesse contexto, em [OLIVEIRA, 2012b]
foi proposto um conjunto de asserções FDR2 que correspondem às condições originais de
[RAMOS, 2011]. Utilizando-se deste trabalho, é possível verificar automaticamente em
FDR2 todas as condições que validam os contratos e a composição entre eles.
A seguir, descrevemos as asserções apresentadas em [OLIVEIRA, 2012b], as quais são
utilizadas por nossa ferramenta, BRIC-Tool-Suport (BTS), como base para a validação
dos contratos e suas composições.
3.1
Análise CSP
Inicialmente, como descrito no capítulo anterior, um componente deve ter o comportamento de um processo de entrada e saída (I/O process). Para isso, ele deve atender às
cinco condições descritas pelas asserções apresentadas na Tabela 3.1.
A primeira asserção diz respeito à condição de Canais de entrada e saída, onde para
um processo P, é verificado se a interseção (inter) dos seus eventos de entrada com
seus eventos de saída é vazia. Para essa verificação é necessária a definição de duas funções: inputs(P) e outputs(P), as quais retornam os eventos de entrada e de saída
de um componente, respectivamente. Na definição da asserção, foram criados os proces-
3.1 Análise CSP
Canais de entrada e saída
Traces infinitos
Ausência de divergência
Entrada determinística
Saída fortemente decisiva
37
assert not Test(inter(inputs(P),outputs(P)) == {})
[T= ERROR
assert not HideAll(P): [divergence free [FD]]
assert P: [divergence free [FD]]
assert LHS_InputDet_A(P) [F= RHS_InputDet(P)
assert LHS_OutputDec_A(P) [F= RHS_OutputDec_A(P)
assert LHS_OutputDec_B(P, c1) [F= RHS_OutputDec_B(P, c1)
assert LHS_OutputDec_B(P, c2) [F= RHS_OutputDec_B(P, c2)
Tabela 3.1: Teste de Caracterização da Composição em Interleave
sos ERROR e Test, com os respectivos comportamentos: ERROR = error -> SKIP e
Test(c) = not c & ERROR. Nessa verificação, inicialmente Test recebe uma condição booleana, cujo valor é representado pela verificação da interseção entre as inputs
e outputs ser vazia ou não. Caso o valor de c seja verdadeiro, o processo Test nega
a condição e bloqueia o processo, fazendo com que Test não refine ERROR. Porém, essa
condição é negada, o que torna a verificação verdadeira.
A verificação que determina se um processo é livre de divergência, está incluído no
próprio FDR2. Já para a verificação de traces infinitos, é usada uma função chamada
Hideall que recebe um processo e esconde todos os seus eventos de entrada (inputs)
e saída (outputs). Como a ocultação dos eventos de um processo que possui traces
infinitos gera divergência, a afirmação da asserção é dada através de sua negação.
As verificações de entrada determinística e saída decisiva exigem um nível de complexidade bem maior em sua implementação, como descrito a seguir.
A entrada determinística é teoricamente definida como o seguinte:
Entrada Determinística. Um processo P possui entrada determinística se
∀s ˆ hc.ai : traces(P ) | c.a : inputs(c, P ) • (s, {c.a}) 6∈ f ailures(P )
Informalmente, isso significa que se um conjunto de eventos de entrada em P é oferecido ao ambiente, nenhum desses deve ser recusado.
A ideia geral dessa propriedade é verificar se o comportamento dos eventos de entrada
de um processo é determinístico. Um processo é dito determinístico se, ao executarmos
duas cópias do mesmo processo, ele comporta-se exatamente da mesma forma.
A solução para essa definição foi verificar o refinamento de falha entre dois processos:
LHS_InputDet_A e RHS_InputDet, os quais descreveremos a seguir. Inicialmente,
são executadas duas cópias de um processo, que sincronizam em um evento chamado
clunk. Este evento sincroniza as cópias do processo depois de cada evento. Inicialmente,
3.1 Análise CSP
38
isto é obtido pela execução do processo em paralelo com o outro, que força a produção
do clunk depois de executar um evento.
Channel clunk
AllButClunk = diff(Events, clunk)
onde AllButClunk é o conjunto de todos os eventos de P com exceção do clunk.
Clunking(P) = P [| AllButClunk |] Clunker
Clunker = [] x:
AllButClunk @ x -> clunk -> Clunker
Podemos observar que Clunking comporta-se exatamente como P, exceto que ele comunica clunk entre cada sincronização de eventos. Depois são executadas cópias do
processo em paralelo, sincronizando unicamente no clunk.
(Clunking(P) [| clunk |] Clunking(P)) \
clunk
Nesse caso, ambas as cópias dos processos executam independentemente, mas suas sequências de traces nunca terão tamanho cuja diferença seja maior do que um, pois sempre que
um dos processos executar um evento, esse aguardará a execução do outro para que ambos
possam sincronizar no evento clunk.
Se P é um processo determinístico e uma cópia de P executa um evento, a outra não
pode recusar. Nesse contexto, ambas as cópias devem ter o mesmo trace.
RHS_InputDet(P) =
(Clunking(P) [|cluck|] Clunking(P)) \
clunck
[|AllButClunck|]
Repeat
Repeat = [] x:
AllButClunck @ x -> x -> Repeat
Dessa forma, o processo RHS_InputDet força as duas cópias do processo a executarem o mesmo trace, por sincronizá-los com o processo Repeat e esse faz com que o evento
sincronizado seja executado duas vezes. Com isso, nunca teremos o comportamento de
deadlocks, já que esse só ocorre se, depois da execução de traces da forma ha, a...d, di, onde
um processo P executa ha, ..., di, uma cópia de P aceita um evento e a outra recusa.
Voltando à Tabela 3.1, podemos comprovar o determinismo no modelo de falhas verificando se RHS_InputDet(P) refina o seguinte processo sobre F (falhas).
3.1 Análise CSP
39
Deterministic(S) =
STOP
|˜|
([] x:AllButClunk @ x ->
(if member(x,S) then
x -> Deterministic(S)
else
(STOP |˜| x -> Deterministic(S))))
LHS_InputDet(P) = Deterministic(inputs(P))
assert LHS_InputDet(P) [F= RHS_InputDet(P)
O processo LHS_inputDet(P) especifica um comportamento determinístico do conjunto de eventos de entradas de um dado processo (inputs(P)), tal que a função
Deterministic executa um evento pertencente a AllButClunk, caso esse faça parte
das entradas de P, é executada em seguida outra cópia desse evento. Como estamos focando apenas no comportamento determinístico para os eventos de entrada, em qualquer
outro momento o processo pode travar.
Finalizando o conjunto de asserções da Tabela 3.1, apresentaremos a seguir a verificação da saída fortemente decisiva, a qual é definida da seguinte maneira:
Saída fortemente decisiva. Um processo P possui saída fortemente decisiva se:
∀s ˆ hc.bi : traces(P ) | c.b : outputs(c, P )•
(s, outputs(c, P )) 6∈ f ailures(P ) ∧ (s, outputs(c, P ) \ {c.b}) ∈ f ailures(P )
Isso significa que todas as escolhas entre eventos de saídas de um determinado canal
em P são internas. Esse não determinismo na saída fornece ao processo a capacidade
de fazer decisões internas baseadas nas entradas. Em um processo com saída fortemente
decisiva, dado o trace s ˆ hc.bi tal que c.b pertence a saída de P , toda saída em c será
recusada, exceto c.b - representado por (s, outputs(c) \ {|c.b|}) ∈ f ailures(P ). Com isso,
é nota-se que o processo sempre irá oferecer uma saída nesse canal.
A solução para Saída fortemente decisiva é dividida em duas partes: a primeira condição verifica se depois da execução de uma trace s ˆ hc.xi, o processo não pode recusar
todos os eventos em {|c|}, o qual representa o conjuntos de todos os eventos através do
canal c). A primeira verificação é feita para todo o processo de uma só vez.
3.1 Análise CSP
40
Considerando o processo Clunker(P) descrito anteriormente, temos duas cópias que
sincronizam no evento clunk e em todos os outros, exceto os valores de outputs(P)
que representam o conjunto de eventos de saída de todos os canais de um processo.
(Clunking(P) [| diff(Events, outputs(P))|] Clunking(P)) \ { clunk }
O processo One2Many executa os eventos de um processo e que não fazem parte dos
canais de saída. Caso ocorra uma saída, é forçada outra comunicação neste canal.
One2Many(S) =
([] x:diff(Events,union(S,{ clunk })) @ x -> One2Many(S))
[] ([] c:S @ [] x:
{|c|} @ x -> One2Many’(S,c,x))
One2Many’(S,c,x) =
[] y:{|c|} @ y -> if x==y then One2Many(S) else STOP
Colocando esse processo em paralelo com os descritos acima, temos o primeiro lado da
asserção apresentado a seguir:
RHS_OutputDec_A(P) =
(Clunking(P) [|diff(Events, outputs(P))|] Clunking(P)) \ {clunck}
[| AllButClunk |]
One2Many(outputs(P))
O processo RHS_OutputDec_A(P) sincroniza as cópias do processo em todos os
eventos, menos os de saída. Quando ocorrer um evento de saída, uma cópia irá sincronizar
com o processo One2Many que em seguida aguardará o evento de saída da outra cópia.
O teste só continuará sendo executado se ambas as cópias realizarem o mesmo evento.
Assim, todas as vezes que o teste carregar, ambas as cópias de P devem realizar o mesmo
trace. O resultado dessa implementação é testada contra a especificação a seguir:
LHS_OutputDec_A(P) =
STOP
|˜|
([] x:diff(Events,union(outputs(P),{ clunck }))
@ x -> LHS_OutputDec_A(P))
[]
([] x:outputs(P) @ x -> (|˜| y:chan(x,P)
@ y -> LHS_OutputDec_A(P)))
onde
3.1 Análise CSP
41
chan(ev,P) =
inter(outputs(P),
{| c | c <- GET_CHANNELS(P), member(ev,{|c|})|})
e a função GET_CHANNELS(P) retorna todos os canais do processo.
No processo LHS_OutputDec_A os eventos de P são executados normalmente até
ocorrer um evento pertencente a saída, que força a execução de outro evento no mesmo
canal, através da função chan. Além disso, é considerado que o processo pode a qualquer
momento travar, por isso existe uma escolha interna entre executar o comportamento
descrito por LHS_OutputDec_A ou STOP.
Assim, o refinamento LHS_OutputDec_A [F= RHS_OutputDec_A(P) checa que
depois de todos os traces t do processo P, a ocorrência de uma saída em um canal é sempre
acompanhada por um evento desse mesmo canal na cópia. Ou seja, essa asserção verifica
que caso um determinado trace t possa ser seguido de uma saída no canal c, o processo
não pode recusar todas as saídas em c. No entanto, esse refinamento não verifica se um
processo é não determinístico para um dado canal de saída. Sendo assim, é necessária
uma verificação adicional para garantir uma escolha não determinística nesse canal.
A segunda condição para se ter uma saída fortemente decisiva é verificar que depois
do trace sˆhc.xi, o processo pode recusar todos os eventos em {|c|} \ {c.x}. Assim, o
processo é não-determinístico para as saídas no canal.
A asserção a seguir verifica individualmente cada canal no processo. Por exemplo,
supondo o alfabeto de P igual a hc1, c2i, são necessárias as seguintes asserções:
assert LHS_OutputDec_B(P,c1) [F= RHS_OutputDec_B(P,c1)
assert LHS_OutputDec_B(P,c2) [F= RHS_OutputDec_B(P,c2)
Nessa parte da verificação, o refinamento garante que em cada saída de P que for
bloqueada, o deadlock deve ocorrer sempre no mesmo trace.
Para mais detalhes sobre a verificação formal de entrada determinística e saída fortemente decisiva, consulte [OLIVEIRA, 2012a].
Além da análise descrita na Tabela 3.1, que caracteriza toda as condições que um
processo deve atender para poder ser composto de forma segura, foram definidos outros
conjuntos de asserções voltados para verificação dos processos, auxiliando nas regras de
composição.
3.1 Análise CSP
42
Análise de Composição
A composição em interleave é a mais simples de todas.
Nessa regra, para dois
processos P e Q, não deve existir eventos em comum entre eles.
Para isso, é utili-
zado o processo RUN que executa todos os eventos da interseção entre dois processos
(inter(events(P),events(Q)), tal que events é uma função que recebe um processo e realiza a união (union) entre os seus eventos de entrada e seus eventos de saída).
Para que essa condição seja válida, a interseção entre os processos deve ser vazia e consequentemente, seus traces serão vazios. Nesse contexto, seu resultado deve refinar os traces
de STOP. Como apresentado na asserção a seguir.
assert STOP [T= RUN(inter(events(P),events(Q)))
As próximas regras apresentam um nível de complexidade maior, já que lidam com a
interação entre os componentes. Como discutido no capítulo anterior, a composição em
comunicação requer que o protocolo tenha entrada e saída confluente, forte compatibilidade e satisfaça a propriedade de saída finita. A seguir apresentaremos o conjunto de
asserções que verificam essas propriedades.
As asserções descritas em [OLIVEIRA, 2012b] foram definidas para um estudo de caso
manual, que gerou e analisou toda especificação em um único módulo, ou seja, de forma
genérica, onde, através da função “apply”, do FDR2, pega vários processos de uma só vez
e aplica a verificação. Logo, algumas alterações foram necessárias, como a retirada dessa
função. Em nossa ferramenta a descrição e análise são realizadas de forma específica,
ou seja, para processos (contratos) individuais descritos na BTS, que será apresentado
no próximo Capítulo. Tomando como base esse exemplo, acrescentamos que todas as
modificações realizadas foram em nível de código CSP, tentando buscar a adaptação do
conjunto de verificações a o que propõe a ferramenta. Essas verificações representam a
implementação das propriedades descritas na Seção 2.3 que validam a composição entre
componentes.
Inicialmente, apresentaremos o grupo de asserções que validam a propriedade de entradas e saídas confluentes.
Todas as verificações descritas a partir desse ponto são voltadas para os protocolos
dos processos.
Iniciamos verificando se o protocolo do processo P é livre de divergência, tal que
PROT_IMP_P representa a implementação do processo sobre um canal.
3.1 Análise CSP
43
assert PROT_IMP_P :[divergence free [FD]]
Logo em seguida é verificado se este de fato é um protocolo válido para um determinado canal no processo P, ou seja, ele deve ser refinado pela projeção de P sobre um
canal. Além disso, também é verificado se o protocolo é um refinamento dessa projeção.
Essas duas verificações garantem que protocolo do processo P possui os mesmos traces de
sua projeção sobre um canal.
assert PROT_IMP_P [F= PROT_IMP_def(P, ip)
assert PROT_IMP_def(P,ip) [FD= PROT_IMP_P
Foram definidas asserções para verificar se todos os eventos da entrada ou da saída
de um protocolo fazem parte das produções de um único canal. Para isso é realizada
uma interseção entre os eventos de entrada do processo P com os eventos do canal ip
(inputs_PROT_IMP(P, ip)). Logo em seguida, através da função subseteq é verificado se todos esses eventos de entrada do processo fazem parte das produções de um
único canal. O resultado é analisado através dos dois processos utilizados na verificação
de Canais de entrada e saída (Tabela 3.1) Test e ERROR.
assert not Test(subseteq(inputs_PROT_IMP(P, ip), {|ip|})) [T= ERROR
assert not Test(subseteq(outputs_PROT_IMP(P, ip), {|ip|})) [T= ERROR
A última asserção que valida a condição de entrada e saída confluente verifica se uma
renomeação do protocolo é determinística.
assert InBufferProt(PROT_IMP_R(P,ip ,R_IO(P,ip,oq))):[deterministic[F]]
tal que R_IO(P,ip,oq) é uma função que recebe dois canais (ip, oq) e renomeia
os dados de oq pelos dados de saída de ip. Por exemplo, para o evento ip.x ∈
outputs(ip) será descrito o evento oq.x. Isso significa que o canal de entrada de
um processo será renomeado com os dados do canal de saída do outro. Em seguida, a
função PROT_IMP_R substitui o canal renomeado oq no protocolo de ip, verificando se
esse tem o comportamento determinístico. Como os canais são representados pela saída
de P e a entrada do outro processo, respectivamente, o resultado dessa substituição sendo
determinístico, implica dizer que no envio de informação para o outro processo não terá
problema no recebimento.
O segundo conjunto de verificações para a composição em comunicação analisa a compatibilidade de protocolo. Essa análise é referente a versão renomeada desses protocolos
(PROT_IMP_R), descrita na verificação de entrada e saída confluente.
3.1 Análise CSP
44
A primeira asserção verifica se o protocolo PROT_IMP_R é livre de deadlocks. Em
seguida, é verificado se ele é um protocolo de comunicação, tanto na entrada como na
saída, igualmente as asserções anteriores, porém essas verificam o comportamento de
PROT_IMP_R. Essas verificações são realizadas para validar a descrição dos protocolos
renomeados.
assert PROT_IMP_R(P, ip,R_IO(P,ip,oq)):[deadlock free [FD]]
assert not Test(subseteq(inputs(PROT_IMP_R(P, ip,R_IO(P,ip,oq)), {|ip|}))
[T= ERROR
assert not Test(subseteq(outputs(PROT_IMP_R(P, ip,R_IO(P,ip,oq)),{|ip|}))
[T= ERROR
Nessa parte, analisamos também o comportamento do Dual-protocol. Inicialmente,
verificamos se o conjunto de eventos de entrada de um protocolo é igual ao conjunto de
eventos de saída do seu dual-protocol.
assert not Test(inputs(PROT_IMP_R(P, ip,R_IO(P,ip,oq))) ==
outputs(DUAL_PROT_IMP_R(P, ip,R_IO(P,ip,oq)))) [T= ERROR
Para uma análise mais segura, também é verificado se o protocolo e seu dual possuem
traces equivalentes.
assert DUAL_PROT_IMP_R(P, ip,R_IO(P,ip,oq)) [T= PROT_IMP_R(P,
ip,R_IO(P,ip,oq))
Finalizando, a analise de protocolo fortemente compatível pode ser definida por verificar se o dual-protocol de um protocolo P é refinado pelo protocolo Q.
assert DUAL_PROT_IMP_R(P, ip,R_IO(P,ip,oq)) [F= PROT_IMP_R(Q,
iq,R_IO(P,ip,oq))
Verificada todas as condições acima, a propriedade de saída finita é caracterizada
pela asserção que exclui todos os eventos de saída de um protocolo, mas não introduz
divergência, como apresentado a seguir:
assert PROT_IMP_R(P, ip,R_IO(P,ip,oq)) \ allOutputs:[divergence free [FD]]
A composição por feedback impõe as mesmas restrições da composição por comunicação descritas anteriormente, exceto que adicionalmente analisa a condição de que canais
sejam desacoplados, como descrito a seguir.
assert INTER_PROT_IMP(P, ip,oq) [F= PROJECTION(P, ip, oq)
3.1 Análise CSP
45
assert PROJECTION(P, ip,oq) [FD= INTER_PROT_IMP(P, ip, oq)
A análise para a propriedade de canais desacoplados recebe dois canais de um processo e realiza uma verificação através de um refinamento bidirecional entre a projeção de P sobre os canais e a intercalação da implementação dos protocolos, tal que
(INTER_PROT_IMP) gera um interleave entre os protocolos dos canais descritos na entrada e PROJECTION retorna a projeção de dois canais sobre o processo P.
Concluindo, a composição reflexiva possui, adicionalmente, a verificação de Compatibilidade de Auto-Injeção com Buffer, que estabelece comunicação entre canais de um
mesmo processo via buffer sem introduzir deadlocks, como descrito a seguir:
assert not PROJECTION(P,ip, oq) [| {| ip, oq |} |] BUFF_IO_1(P_LR1, P_LR2)
:[deadlock free [F]]
onde a PROJECTION do processo P sobre dois canais é colocado em paralelo com o
processo BUFF_IO_1 que recebe dois conjuntos de eventos de comunicação P_LR1 e
P_LR2, renomeia seus canais e os coloca em interleave. O interleave desses sincronizando
em paralelo com a projeção de um processo sobre esses dois canais deve ser livre de
deadlock.
Utilizando esse conjunto de verificações foi possível aplicar a abordagem para o desenvolvimento sistemático e confiável em uma verificação automática através da ferramenta
apresentada no próximo capítulo.
46
4
BTS: Ferramenta de suporte ao
desenvolvimento de sistemas confiáveis
baseados em componentes
Nessa seção apresentaremos todo processo de construção da ferramenta BTS (BRICTool-Support). Começaremos apresentando os detalhes técnicos, como linguagem de programação e ferramentas utilizadas. Em seguida, apresentaremos a estrutura da ferramenta, bem como sua funcionalidade. Por fim, será apresentada a aplicação prática da
estratégia pela BTS.
4.1
Detalhes Técnicos
A ferramenta foi implementada utilizando a linguagem de programação Java e a IDE
NetBeans. Além disso, a fim de realizar as verificações necessárias nos scripts CSP gerados, BTS foi integrada a duas ferramentas de suporte CSP:
• TypeChecker (verificador de tipos da linguagem CSP) é utilizado para verificar se
o comportamento CSP descrito pelo usuário está tipado corretamente.
• FDR2 (Failures-Divergence Refinement) é utilizado através do controle direto, sem interface gráfica. Para isso utilizamos a interface Batch [BROWNLEE,
2000] para executar o FDR2 através de linhas de comando. Este é responsável pela
verificação das asserções dos componentes do sistema, tanto na criação, como na
composição. Em caso de falha na verificação, as razões da falha são retornadas por
essa ferramenta.
4.2 Ferramenta BTS
4.2
47
Ferramenta BTS
A ferramenta foi desenvolvida para auxiliar o usuário na criação e verificação do
componente e de sua composição. O diagrama de caso de uso descrito na Figura 4.1
apresenta as ações que podem ser realizadas no sistema para completar o processo da
BTS.
Figura 4.1: Diagrama de Caso de Uso da BTS
A Figura mostra o usuário e sua interação com o sistema que é descrito através dos
seguintes casos de uso:
1. Usuário cria as interfaces do componente.
2. Usuário cria porta de comunicação do componente.
3. Usuário cria contrato de componente.
4. Define instancias a partir do contrato criado
5. Realiza a verificação da composição entre componentes.
4.2 Ferramenta BTS
48
Cada caso de uso, na ordem descrita, sempre inclui o anterior. Além disso, podemos
observar uma interação do sistema com a ferramenta FDR2.
Para entendermos a sequência de eventos que determina o comportamento desses casos
de uso, a Figura 4.2 apresenta o diagrama de sequência para o caso de uso criação de
interface de componente. Como podemos observar, através da interface de tipos (Fig. 4.3),
o usuário descreve tipos como intervalo, booleanos e datatype. Internamente a ferramenta
cria o tipo e adiciona em uma lista.
Figura 4.2: Diagrama de sequência da criação de tipos
A mesma sequência de passos ocorre na criação de canais. A figura 4.4 apresenta sua
interface de interação com o usuário. Nela, podemos observa a respectiva lista de tipos
criada anteriormente, que representarão os valores comunicados pelo canal.
Na figura 4.5 podemos visualizar a sequência de eventos que determina o comportamento do caso de uso criar contrato de componente. Inicialmente o usuário descreve as
informações do contrato, como nome, comportamento e canais. Ao descrever o comportamento (representado por um processo CSP), é criado o objeto CheckerBehavior que
executa o TypeChecker e verifica se o comportamento está tipado corretamente, pega a
√
saída e apresenta ao usuário através do
verde, para as saídas corretas (como visto na
Figura 4.6 - A) e um χ vermelho, caso contrário.
Logo após, através da interação do usuário (Fig. 4.6 - B), a ferramenta verifica se
4.2 Ferramenta BTS
49
Figura 4.3: Interface para criação de tipos
Figura 4.4: Interface para criação de canais
o contrato atende as condições e propriedades apresentadas em [RAMOS, 2011] (I/O
process), através do objeto VerificationContract, que cria um arquivo CSP a partir dos
valores de entrada e gera as asserções. Em seguida comunica-se com a ferramenta FDR2,
que faz a verificação e registra o resultado em um arquivo de log. A ferramenta ler esse
4.2 Ferramenta BTS
Figura 4.5: Diagrama de sequência da criação de contrato
50
4.2 Ferramenta BTS
51
Figura 4.6: Interface para criação de contrato
resultado e faz uma análise. O resultado é apresentado ao usuário através da interface
descrita na Figura 4.7. Depois o contrato é criado e salvo em uma lista.
Figura 4.7: Tela de resultado
A sequência de passos para a instanciação difere do contrato apenas na entrada de
dados, onde na instância o usuário apenas renomeia o nome do contrato e dos seus respectivos canais (Fig. 4.8). Internamente são seguidos os mesmos passos que o contrato.
Na verificação da composição, o usuário seleciona os componentes e a regra de verificação a partir da interface descrita na Figura 4.10. Como observado no diagrama de
sequência da Figura 4.9, a BTS cria o objeto CSPVerificationRule que gera o arquivo
4.2 Ferramenta BTS
52
Figura 4.8: Tela de instanciação
com a especificação CSP, de acordo com a regra selecionada. Assim como na criação do
contrato, comunica-se com a ferramenta FDR2, faz a verificação salvando o resultado em
um arquivo. A BTS analisa esse resultado e caso a composição seja válida, é gerado um
novo componente de acordo com as entradas e a regra de composição, e o resultado é
apresentado ao usuário.
Estrutura da ferramenta de suporte
A BTS foi construída para receber dados, gerar especificação CSP automaticamente,
verificar e apresentar ao usuário o resultado da verificação (Figura 4.11). As especificações
CSP são geradas de acordo com a descrição inicial do usuário, bem como as regras e
restrições descritas em [RAMOS, 2011].
Do ponto de vista do usuário podemos dizer que nossa ferramenta é dividida em duas
etapas: Contrato de componente e composição (Fig. 4.12). Na etapa de contrato de componente, a ferramenta de suporte recebe como entrada os tipos, canais e comportamento
CSP. A saída da ferramenta apresenta o resultado da verificação das condições impostas
na Seção 2.3 e gera o componente que será adicionado a uma lista.
Na etapa de composição, a ferramenta recebe um ou dois componentes que foram
definidos na etapa anterior. Sua saída é o resultado das verificações realizadas de acordo
4.2 Ferramenta BTS
53
Figura 4.9: Diagrama de sequência da composição
Figura 4.10: Tela de Composição
4.2 Ferramenta BTS
54
Figura 4.11: Estrutura da BTS
Figura 4.12: Entradas e saídas da BTS
com a regra de composição selecionada e as restrições impostas para essa regra. Além
disso, a composição gera um novo componente.
A ferramenta garante confiabilidade através da geração interna da especificação CSP
e verificação através do FDR2.
Funcionamento da ferramenta de suporte
A ferramenta BTS possui uma interface amigável e esconde todo conjunto de verificações apresentado no Capítulo 3, ou seja, o usuário não precisa ter conhecimento sobre
a ferramenta FDR2. No entanto, a necessidade de conhecimento em CSP ainda se faz
necessária. A remoção dessa necessidade será motivação para trabalhos futuros interessantes. A Figura 4.13 apresenta a interface inicial da BTS. Esta apresenta quatro opções:
1) Criação de tipos, 2) Criação de canais, 3) Criação de contrato, 4) Criação de instâncias. Inicialmente são definidos os tipos, que representam a interface do contrato. Os
canais representam as portas de comunicação do contrato, que são associados aos tipos
de dados. Após a definição de tipos e canais, podemos definir nosso modelo de contrato
e posteriormente, instanciar esse contrato para ser composto.
Na tela de descrição de tipos o usuário pode definir tipos CSP automaticamente. Por
4.2 Ferramenta BTS
55
Figura 4.13: Interface BTS
exemplo, a criação de um intervalo é realizada através da definição de um nome e seu
valor mínimo e máximo (Fig. 4.3). Já a tela de criação de canais apresenta uma lista
com todos os tipos criados na tela anterior. O usuário define um nome para o canal e o
relaciona a um tipo ou mais (Fig. 4.4).
A tela de contrato recebe um nome (que representará o nome do componente) e o comportamento CSP. Além disso, para cada canal, o usuário deve definir quais eventos fazem
parte do conjunto de entrada e quais fazem parte do conjunto de saída do componente.
Sendo também necessário definir para esses canais o protocolo e o seu dual-protocol.
Finalizando, após a definição de um contrato de componente, é possível instanciá-lo
gerando novos componentes.
4.2.1
Aplicação prática da estratégia pela BTS
Como vimos na seção anterior, internamente a BTS gera arquivos CSP que são verificados pelo FDR2. Nessa seção apresentaremos a estruturação desses arquivos e também
apresentaremos a utilidade do typeChecker.
Todo conjunto de entrada é especificado na BTS, menos o comportamento do com-
4.2 Ferramenta BTS
56
ponente que é um processo CSP descrito pelo usuário. Quando a ferramenta recebe esse
comportamento, antes de ser integrado ao resto da especificação para que as asserções
sejam analisadas, é necessário fazer uma verificação, visto que esse é suscetível a erros.
A Figura 4.14 mostra um exemplo de como o comportamento especificado pelo usuário
é gerado para verificação. Utilizaremos o exemplo do Cliente-servidor descrito no Capítulo
2. Apresentaremos a seguir o comportamento do componente cliente.
Inicialmente, a BTS declara os tipos, canais e adiciona o comportamento CSP. Em seguida, ela comunica com TypeChecker que faz a verificação de tipagem. O resultado é
√
apresentado ao usuário através da apresentação dos ícones e χ, como descrito na Figura
4.6 – A. A saída do TypeChecker pode ser visualizada através do click sobre esses ícones,
que é descrita na Figura 4.15.
Realizada a verificação pelo TypeChecker a ferramenta está preparada para gerar e
verificar as condições descritas na seção 2.3.
Verificando as condições de I/O Process
A verificação de I/O process é fundamental para que as propriedades e restrições
do componente sejam garantidas e posteriormente a aplicação das regras de composição
tenham o resultado desejado. O arquivo CSP gerado nessa fase é descrito através de um
modelo de contrato que possui as seguintes características:
• Nome
• Comportamento
• Tipos
• Canais
• Eventos de entrada e saída
A partir das características descritas acima, o corpo da especificação (gerada automaticamente) para verificação do comportamento de I/O process, do componente Cliente,
possui a seguinte estrutura:
4.2 Ferramenta BTS
57
NUM = {0..20}
datatype DADOSMQ = rt.NUM | requisitaSaldo | ackRt.Bool | recSaldo.NUM
datatype DADOSCL = insereCartao.NUM | digitaSenha.NUM | retiraDin.NUM |
saldo | retiraCartao | recebeDin | mostraSaldo
channel cl : DADOSCL
channel maq : DADOSMQ
Cliente = cl.insereCartao?num -> cl.digitaSenha?num ->
(SAQUE [] SALDO) ; cl!retiraCartao -> Cliente
SAQUE = cl.retiraDin? val -> maq!rt.val ->
maq.ackRt?a -> cl!recebeDin -> SKIP
SALDO = cl.saldo -> maq!requisitaSaldo ->
maq.recSaldo?x -> cl!mostraSaldo -> SKIP
Figura 4.14: Exemplo de comportamento do componente
Figura 4.15: Interface de saída do TypeChecker
• Declaração de tipos e canais. Estes são descritos através das interfaces das Figuras
4.3 e 4.4. Internamente a BTS transforma em código CSP, como apresentado a
seguir:
NUM = {0..20}
datatype DADOSMQ = rt.NUM | requisitaSaldo | ackRt.Bool | recSaldo.NUM
datatype DADOSCL = insereCartao.NUM | digitaSenha.NUM | retiraDin.NUM |
saldo | retiraCartao | recebeDin | mostraSaldo
channel cl : DADOSCL
channel maq : DADOSMQ
• Processo (Comportamento): descrito pelo usuário.
Cliente = cl.insereCartao?num -> cl.digitaSenha?num ->
(SAQUE [] SALDO) ; cl!retiraCartao -> Cliente
SAQUE = cl.retiraDin? val -> maq!rt.val ->
4.2 Ferramenta BTS
58
maq.ackRt?a -> cl!recebeDin -> SKIP
SALDO = cl.saldo -> maq!requisitaSaldo ->
maq.recSaldo?x -> cl!mostraSaldo -> SKIP
• GET_CHANNEL: conjunto de canais do processo. Essa função é necessária para a
verificação das saídas fortemente decisivas.
GET_CHANNELS(P) =
let f =
<
(Cliente, { cl, maq })
>
within apply(f,P )
• inputs: eventos de entrada do componente.
inputs(P) =
let f =
<
( Cliente, {| maq.ackRt, maq.recSaldo |})
>
within apply(f, P )
• outputs: eventos de saída do componente.
outputs(P) =
let f =
<
( Cliente, {| maq.rt, maq.requisitaSaldo |})
>
within apply(f,P)
• Condições de verificação, apresentadas na seção anterior. Estas representam as cinco
condições que garantes ao componente o comportamento de I/O process.
assert not Test(inter(inputs(Cliente),outputs(Cliente)) == {}) [T= ERROR
assert not HideAll(Cliente):[divergence free [FD]]
assert Cliente:[divergence free [FD]]
4.2 Ferramenta BTS
59
assert LHS_InputDet(Cliente) [F= RHS_InputDet(Cliente)
assert LHS_OutputDec_A(Cliente) [F= RHS_OutputDec_A(Cliente)
assert LHS_OutputDec_B(Cliente,maq) [F= RHS_OutputDec_B(BricRingCell,maq)
assert LHS_OutputDec_B(Cliente,cl) [F= RHS_OutputDec_B(Cliente,cl)
Além disso, o arquivo gerado inclui, na primeira linha, um arquivo ("auxiliar.csp").
Este tem as funções necessárias para realizar as verificações do comportamento de I/O
process descritos em [OLIVEIRA, 2012b], juntamente com as modificações realizadas,
apresentado no Capítulo 3.
Utilizamos o FDR2 para realizar a verificação dessas asserções. O resultado é salvo
em um arquivo que é analisado e repassado para o usuário de maneira bem simples, como
descrito na Figura 4.7. Nela, o resultado de todas as asserções é realizado com sucesso,
√
descrito através do verde. Caso alguma condição não seja atendida, seu resultado será
apresentado como um χ no lugar do ícone verde. Além disso, ainda é possível visualizar
a saída do FDR2 através da opção details.
Para realizar a verificação da composição, que tem os componentes selecionados através da interface descrita na Figura 4.10, antes é necessário instanciar os componentes
(Fig. 4.8) que se deseja compor. Para gerar uma instância de contrato, basta existir um
contrato implementado e verificado. Esse contrato tem o nome e canais renomeados e
internamente esse comportamento é representado pela função rename de CSP.
Verificando a composição
Como descrito no Capítulo 2 existem quatro regras de composição que podem ser
aplicadas entre os componentes e cada uma gera seu conjunto de verificação.
Nessa parte, a BTS recebe um ou dois componentes que são I/O process e define a
seguinte estrutura:
• Corpo do documento. Construído igualmente ao documento que verifica o comportamento de I/O process, exceto a função GET_CHANNEL, que não é necessária
nessa fase, e o conjunto de verificações que é diferente.
• Conjunto de asserções de acordo com regra selecionada. Para cada regra, existe um
conjunto de verificações diferentes, como descrito a seguir:
4.2 Ferramenta BTS
60
Inteleave:
Para duas instâncias do processo Cliente (Cliente1 e Cliente2 ) temos os seguintes
conjuntos de asserções:
--INTERLEAVING COMPOSITION
Cliente1_Cliente2_INTER = INTER(Cliente1,Cliente2)
assert STOP [T= RUN(inter(events(Cliente1),events(Cliente2)))
A composição em interleave é realizada através da função IN T ER(P 1, P 2), tal que
P1 e P2 são processos. A função IN T ER está implementada no arquivo rule.csp, o qual
o arquivo deve importar.
Nessa regra de composição, considerando-se que um componente só pode ser composto caso atenda a condição de I/O process, verificado anteriormente, a única restrição
imposta é que os componentes não devem possuir conjuntos de eventos em comum. A
verificação da composição também é realizada através da ferramenta FDR2 e seu resultado apresentado para o usuário. Além disso, a BTS gera um novo componente representado pelo processo Cliente1_Cliente2_INTER que tem como comportamento a
INTER(Cliente1,Cliente2).
Communication:
Para exemplificar a regra de composição em comunicação, apresentaremos a composição do Cliente1 com a Máquina e os respectivos canais maq1 e maq. Nessa regra o
conjunto de verificação é maior e mais complexo. Com isso, temos as seguintes asserções:
1. maq1 está no alfabeto de Cliente1
assert not Cliente1 \ {|maq1|} [T= Cliente1
2. maq está no alfabeto de Maquina
assert not Maquina \ {|maq|} [T= Maquina
3. Verificação de I/O confluente para o primeiro componente
Nessa fase, as verificações são voltadas para os protocolos dos processos. Inicialmente é verificado se o protocolo do processo Cliente1 sobre o canal maq1 é livre
de divergência. Em seguida verifica se este de fato é um protocolo válido, ou seja,
ele deve ser refinado pela projeção de Cliente1 sobre o canal maq1. Além disso,
também é verificado se o protocolo é um refinamento dessa projeção.
4.2 Ferramenta BTS
61
(a) Ele é livre de divergência
assert PROT_IMP_Cliente1_maq1 :[divergence free [FD]]
(b) Ele é refinado pela projeção sobre um canal
assert PROT_IMP_Cliente1_maq1 [F= PROT_IMP_def(Cliente1,maq1)
(c) Ele é refinamento da projeção sobre um canal
assert PROT_IMP_def(Cliente1,maq1) [FD= PROT_IMP_Cliente1_maq1
(d) Ele é um port-protocol (communication protocol)
Aqui é verificado se todos os eventos da entrada ou da saída de Cliente1
fazem parte das produções do canal maq1. Para isso é realizada uma interseção entre os eventos de entrada de Cliente1 com os eventos do canal
(inputs_PROT_IMP(Cliente1, maq1)). Logo em seguida, através da
função subseteq é verificado se todos esses eventos de entrada do processo
fazem parte das produções de um único canal.
i. Entrada
assert not Test(subseteq(inputs_PROT_IMP(Cliente1,maq1),
{|maq1|})) [T= ERROR
ii. Saída
assert not Test(subseteq(outputs_PROT_IMP(Cliente1,maq1),
{|maq1|})) [T= ERROR
(e) A versão renomeada é I/O Confluente
Essa definição é baseada em [RAMOS, 2011] a qual afirma que um processo
é I/O confluente se possuir ações de canais distintos a serem executadas, e
uma não impedir a outra de ser executada, a menos que seja no mesmo canal.
Esse comportamento foi implementado no trabalho de [OLIVEIRA, 2012b],
através da asserção InBufferProt que verifica se o comportamento de P [[R]]
(PROT_IMP_Cliente1_maq1_R_IO_maq), que renomeia os dados de todos
os canais do componente, mas preserva sua direção, é determinístico.
assert InBufferProt(PROT_IMP_Cliente1_maq1_R_IO_maq, maq1)
:[deterministic [F]]
4. Verificação de I/O confluente para o segundo componente
O conjunto de verificações para o segundo componente são semelhante as do item
3.
4.2 Ferramenta BTS
62
5. Protocolos são fortemente compatíveis
Conjunto de verificações a seguir analisa a compatibilidade de protocolo. Essa
análise é referente a versão renomeada, descrita na verificação de entrada e saída
confluente, apresentada anteriormente. As asserções a seguir verificam se o protocolo
renomeado dos dois componentes é livre de deadlocks.
(a) Protocolos são deadlock-free
i. Na esquerda
assert PROT_IMP_Cliente1_maq1_R_IO_maq
:[deadlock free [FD]]
ii. Na direita
assert PROT_IMP_Maquina_maq_R_IO_maq1
:[deadlock free [FD]]
(b) Protocolos são protocolos de comunicação
Aqui é verificado se os protocolos dos componentes são protocolos de comunicação, tanto na entrada como na saída, igualmente as asserções anteriores,
porém essas verificam o comportamento do protocolo renomeado.
i. Entrada esquerda
assert not Test(subseteq(inputs(
PROT_IMP_Cliente1_maq1_R_IO_maq),{| maq1|})) [T= ERROR
ii. Saída esquerda
assert not Test(subseteq(outputs(
PROT_IMP_Cliente1_maq1_R_IO_maq),{|maq|})) [T= ERROR
iii. Entrada direita
assert not Test(subseteq(inputs(
PROT_IMP_Maquina_maq_R_IO_maq1),{| maq|})) [T= ERROR
iv. Saída direita
assert not Test(subseteq(outputs(
PROT_IMP_Maquina_maq_R_IO_maq1),{| maq1|})) [T= ERROR
(c) Ele é um Dual Protocol
Nessa parte analisamos o comportamento do Dual-protocol para os dois componentes, verificando se o conjunto de eventos de entrada de um protocolo é
igual ao conjunto de eventos de saída do seu dual-protocol.
i. Entrada e saída
assert not Test(inputs(PROT_IMP_Cliente1_maq1_R_IO_maq) ==
outputs(DUAL_PROT_IMP_Cliente1_maq1_R_IO_maq)) [T= ERROR
4.2 Ferramenta BTS
63
ii. Entrada e saída
assert not Test(outputs(PROT_IMP_Maquina_maq_R_IO_maq1) ==
inputs(DUAL_PROT_IMP_Cliente1_maq1_R_IO_maq)) [T= ERROR
iii. O protocolo e seu dual possuem traces equivalentes
A. Esquerda
assert DUAL_PROT_IMP_Cliente1_maq1_R_IO_maq [T=
PROT_IMP_Cliente1_maq1_R_IO_maq
B. Direita
assert PROT_IMP_Cliente1_maq1_R_IO_maq [T=
DUAL_PROT_IMP_Cliente1_maq1_R_IO_maq
A analise de protocolo fortemente compatível é definida através da verificação
do dual-protocol de Cliente1 ser refinado pelo protocolo Maquina, devendo
também ser a verificação contrária verdade.
(d) assert DUAL_PROT_IMP_Cliente1_maq1_R_IO_maq [F=
PROT_IMP_Maquina_maq_R_IO_maq1
(e) Correspondência de compatibilidade
assert PROT_IMP_Maquina_maq_R_IO_maq1 [F=
DUAL_PROT_IMP_Cliente1_maq1_R_IO_maq
6. Protocolo têm propriedade de saída finita
A propriedade de saída finita é caracterizada pela asserção que exclui todos os
eventos de saída de um protocolo, mas não introduz divergência, como apresentado
a seguir:
(a) Esquerda
assert PROT_IMP_Cliente1_maq1_R_IO_maq \
outputs(PROT_IMP_Cliente1_maq1_R_IO_maq)
:[divergence free [FD]]
(b) Direita
assert PROT_IMP_Maquina_maq_R_IO_maq1 \
outputs(PROT_IMP_Maquina_maq_R_IO_maq1)
:[divergence free [FD]]
Todo conjunto de verificações aqui apresentados estão descritos no Capítulo 3.
A geração dos arquivos CSPs para as regras de feedback e reflexive possuem a mesma
estrutura, porém, nessas regras se trata apenas um componente e possuem algumas propriedades de verificação diferentes.
4.2 Ferramenta BTS
4.2.2
64
Considerações Finais
Nesse capítulo apresentamos a BTS, ferramenta desenvolvida durante esse trabalho de
dissertação. Foi feita uma apresentação de sua implementação, estrutura e funcionalidade,
além de mostrarmos alguns exemplos práticos de sua utilização e alguns arquivos gerados
por ela.
A ferramenta faz uma verificação prévia da composição de componentes. Esta implementa a abordagem proposta em [RAMOS, 2011] que apresenta todas as verificações e
validações através do método formal CSP.
A ideia desse trabalho foi buscar o máximo de automação para garantir agilidade na
abordagem de verificação segura. Porém, ainda não foi possível ter um processo totalmente automatizado, devido à descrição do comportamento do componente ser implementado manualmente. Mesmo assim, a BTS já traz grandes benefícios à utilização da
abordagem de Ramos [RAMOS, 2011]. A ferramenta desenvolvida é capaz de, a partir da
definição de um modelo de componente, verificar se sua comunicação com outros componentes é segura. Essa verificação é feita através das características definidas pelo usuário,
como comportamento, portas e interface. Internamente a ferramenta gera arquivos CSP
e realiza a verificação automaticamente. O resultado dessa verificação é transmitido diretamente para o usuário.
Foi realizado um estudo de caso para validar nossa ferramenta, onde foram gerados,
testados e compostos os componentes a partir do exemplo clássico de buffer circular. Este
será apresentado no próximo capítulo.
65
5
Estudo de Caso
Nesse capítulo faremos uma validação inicial de nossa ferramenta para o desenvolvimento sistemático e confiável de componentes. O estudo de caso consiste no exemplo do
buffer circular.
O principal objetivo desse estudo de caso é validar nossa ferramenta utilizando o exemplo descrito em [OLIVEIRA, 2012b] que avaliou o desenvolvimento sistemático e confiável manualmente. Nossa proposta é demonstrar a geração e composição de componentes
sendo gerada automaticamente pela BTS. Além disso, esta reduz toda complexidade da
abordagem descrita na Seção 2.3.
5.1
Buffer Circular
Um buffer consiste em uma região de memória temporária, cujo objetivo é a escrita
e leitura de dados no mesmo. Um buffer circular consiste na utilização de buffers de
tamanho fixo, como se estivessem ligados ponta a ponta.
Em nosso exemplo, o buffer circular (Fig. 5.1) é composto por um anel de células
com um controlador central e uma cache. Cada célula tem sua identificação e é capaz de
armazenar um valor. O controlador é responsável por receber entradas e fornecer saídas
solicitadas pelo ambiente e interagir de acordo com o armazenamento das células.
O anel é modelado como uma sequência de células, com suas extremidades unidas. Já
o controlador recebe os seguintes valores: uma cache, o tamanho do buffer e dois índices
para o anel circular: top e bottom. Caso os valores top e bottom coincidam, não é possível
distinguir se o anel atingiu sua capacidade máxima de armazenamento ou se está vazio.
Por isso, também precisamos do tamanho do buffer.
Na aplicação do estudo de caso definimos os seguintes componentes: Cell, que representa o comportamento de uma célula do buffer e um Controller. A Célula (Fig. 5.2)
tem como comportamento ler ou escrever informações. A descrição CSP de Cell, que
5.1 Buffer Circular
66
Figura 5.1: Buffer Circular
representa o B do contrato BRIC, é apresentada a seguir:
Figura 5.2: Representação do componente Cell
Cell =
let CellState(val) =
rd.req?dumb -> rd.ack!val -> CellState(val)
[]
wrt.req?x -> wrt.ack.x -> CellState(x)
within
CellState(0)
O Controller (Fig. 5.3) é responsável por controlar o recebimento de informações que
serão armazenas e lidas das células. Seu comportamento CSP é descrito a seguir:
Figura 5.3: Representação do componente Controller
5.1 Buffer Circular
67
As ações de entrada do Controller são executadas enquanto o buffer não atingir
seu tamanho máximo (maxbuff). Caso o tamanho do buffer seja vazio, a entrada é
armazenada em cache, o buffer é incrementado e top e bot não mudam. Ou seja, o cache
representa a primeira célula que armazena o dado recebido pelo Controller. Caso o buffer
não esteja vazio, o Controller envia o valor de entrada para o anel, juntamente com a
posição de armazenamento. Essa comunicação é realizada através do canal de escrita.
Os índices e o tamanho do anel são alterados. O maxring representa o limite do anel
(definido por maxbuff - 1), como apresentado nas ações a seguir:
InputController(cache,size,top,bot) =
size < maxbuff & input?x ->
(size == 0 & ControllerState(x,1,top,bot)
[]
size > 0 & write.top.req!x -> write.top.ack?dumb ->
ControllerState(cache,size+1,(top%maxring)+1,bot))
Nas ações de saída, que só serão executadas se o buffer não estiver vazio, o valor
registrado em cache será sempre o valor que está sendo comunicado. Caso o buffer tenha
um único elemento, este será comunicado e seu tamanho atualizado. Se existem elementos
armazenados em qualquer célula, o valor de x é lido, o cache é atualizado com esse valor
e bot é incrementado. Essas ações do comportamento do Controller são apresentadas a
seguir:
OutputController(cache,size,top,bot) =
size > 0 & output!cache ->
(size > 1 & read.bot.req?dumb -> read.bot.ack?x ->
ControllerState(x,size-1,top,(bot%maxring)+1)
(|~| dumb:Value @ read.bot.req.dumb -> read.bot.ack?x ->
ControllerState(x,size-1,top,(bot%maxring)+1))
[]
size == 1 & ControllerState(cache,0,top,bot))
O comportamento de Controller inicia com a cache e o tamanho do buffer vazios e top
e bot na primeira posição. Depois de inicializado, a opção de escolha entre InputController
e OutputController é oferecida.
5.2 Aplicação do Buffer Circular na BTS
68
ControllerState(0,0,1,1)
InputController(cache,size,top,bot)
[]
OutputController(cache,size,top,bot)
5.2
Aplicação do Buffer Circular na BTS
Para verificar o desenvolvimento sistemático de componentes através da BTS, primeiramente devemos considerar as seguintes características:
• Cada célula do buffer utiliza dois canais de comunicação: wrt para escrita e rd para
leitura.
• O Controller utiliza os seguintes canais de comunicação: write para escrita e read
para leitura, input e output para receber e fornecer dados do ambiente externo.
• Toda comunicação da célula com o controlador tem duas direções: (req) que representa uma requisição de leitura ou escrita e (ack) como uma confirmação.
Essas características representam os tipos e canais CSP que são descritos através das
interfaces nas figuras 4.3 e 4.4, respectivamente.
Na criação de tipos, o usuário define a interface que será utilizada na construção do
componente. Com isso, descrevemos o conjunto de interfaces (I) do contrato BRIC.
O conjunto de canais (C) e sua relação com a interface (R = C → I) é definido na
Figura 4.4, onde o usuário cria o canal e seleciona os tipos que farão parte da comunicação.
Por exemplo, nessa tela temos a criação de um canal wrt que tem como interfaces uma
direção (Direction) e um valor (Value).
5.2.1
Contrato BRIC de Cell e Controller
Como apresentado na Seção 2.3, um contrato de componente possui um comportamento (processo CSP), portas (canais) e interface (tipos). Os contratos que representam
a Cell e o Controller, descritos nas Figuras 5.2 e 5.3 são definidos a seguir e representam
os valores de entrada da ferramenta:
*



rd 7→ Direction x V alue, 
+
CtrCell = Cell, 
, {Direction x V alue}, {rd, wrt}
wrt 7→ Direction x V alue 
5.2 Aplicação do Buffer Circular na BTS


*
69

read 7→ CellId x Direction x V alue, 
CtrController = Controller, 
,
write 7→ CellId x Direction x V alue 
{ CellId x Direction x Value}, {read, write} i
Para demonstrarmos comos esses dados são descritos na BTS, apresentaremos a criação do contrato CtrCell . A Figura 4.6 nos apresenta a tela de contrato, onde definimos
o comportamento B e a lista de canais, que possuem os tipos associados representando a
relação de um para o outro.
Além do conjunto de entradas que representam o contrato BRIC, a descrição dos
eventos de entrada e saída, apresentadas a seguir, são definidos através da interface na
Figura 5.4, onde o usuário seleciona o canal e define manualmente o canal de comunicação,
seja para a entrada ou para a saída. No exemplo da Figura, está sendo definido o valor
de inputs para o canal rd.
Figura 5.4: Interface para descrição de eventos de entrada e saída
inputs(rd, CtrCell ) = {|rd.req|}
inputs(wrt, CtrCell ) = {|wrt.req|}
outputs(rd, CtrCell ) = {|rd.ack|}
outputs(wrt, CtrCell ) = {|wrt.ack|}
inputs(read.1, CtrController ) = {|read.1.ack|}
inputs(read.2, CtrController ) = {|read.2.ack|}
inputs(read.3, CtrController ) = {|read.3.ack|}
inputs(write.1, CtrController ) = {|write.1.ack|}
inputs(write.2, CtrController ) = {|write.2.ack|}
inputs(write.3, CtrController ) = {|write.3.ack|}
inputs(input, CtrController ) = {|input|}
outputs(read.1, CtrController ) = {|read.1.req|}
5.2 Aplicação do Buffer Circular na BTS
70
outputs(read.2, CtrController ) = {|read.2.req|}
outputs(read.3, CtrController ) = {|read.3.req|}
outputs(write.1, CtrController ) = {|write.1.req|}
outputs(write.2, CtrController ) = {|write.2.req|}
outputs(write.3, CtrController ) = {|write.3.req|}
outputs(output, CtrController ) = {|output|}
Descrito esse conjunto de definições de entrada, todas as outras características, como
verificação e composição são gerados automaticamente. Inicialmente, para cada contrato
descrito, a ferramenta verifica se esse possui o comportamento de I/O process. Para isso,
internamente é gerado o arquivo CSP que possui toda descrição do contrato juntamente
com o conjunto de verificações que é analisado pelo FDR2.
Concluindo que CtrCell e CtrController são contratos válidos, agora é possível compor
esses componentes. O contrato de cada célula descrita na Figura 5.1 é definido como uma
instância de CtrCell .
Cell1 = Inst(CtrCell , {rd 7→ rd_i.1, wrt 7→ wrt_i.1})
Cell2 = Inst(CtrCell , {rd 7→ rd_i.2, wrt 7→ wrt_i.2})
Cell3 = Inst(CtrCell , {rd 7→ rd_i.3, wrt 7→ wrt_i.3})
onde Cell1, Cell2 e Cell3 possuem o mesmo comportamento que Cell, porém, com os
canais renomeados e cada instância representa um contrato de componente válido.
5.2.2
Composição
Para realizar a verificação da composição é necessário gerar o protocolo para cada
canal do componente. Na descrição do contrato existe a opção, para cada canal, de
adicionar seu protocolo e dual-protocol, que são representados por processos CSP, como
podemos observar na Figura 5.5. Na Figura, encontramos a definição do protocolo e dual
de Cell sobre o canal rd, estes estão representados como uma chamada de função, pois os
processos que os representam foram definidos anteriormente em "auxiliar process", opção
que a BTS fornece ao usuário, para definir processos que ele deseja inserir no arquivo da
especificação final. Em nosso estudo de caso, temos os seguintes protocolos e protocolos
dual para Cell e Controller:
P rotCell(e) =|˜| v2 : V alue @ e.req?v1 → e.ack.v2 → P rotCell(e)
5.2 Aplicação do Buffer Circular na BTS
71
Figura 5.5: Interface para descrição protocolo e dual-protocols
Dual_P rot_Cell(e) = |˜| v1 : V alue @ e.req.v1 → e.ack?v2 → Dual_P rotCell(e)
P rotController(e) =|˜|v1 : V alue @ e.req.v1 → e.ack?v2 → P rotController(e)
Dual_P rotController(e) = |˜| v2 : V alue @ e.req?v1 → e.ack.v2 → Dual_P rotController(e)
Para analisar o comportamento das composições, a BTS nos fornece a interface descrita na Figura 5.6, onde no exemplo da Figura temos a seleção de dois componentes
(Cell1 e Cell2 ) e da regra de interleaving. Como nessa regra não são necessários os canais
(port), estes não precisam ser descritos. Apresentaremos a seguir a ordem da aplicação
das regras pela BTS.
Figura 5.6: Tela de composição com o exemplo da composição em interleave
5.2 Aplicação do Buffer Circular na BTS
72
Interleave
Nesse estudo de caso, a composição em interleave consiste em validar a comunicação
entre as três células que formam o anel de buffer (Fig. 5.1). Primeiramente, compomos
em interleave Cell1 e Cell2.
Figura 5.7: Composição em interleave de Cell1 e Cell2
Cell1_Cell2 = Cell1 [|||] Cell2
Para que a aplicação da regra seja válida, basta que seus conjuntos de eventos, o que é
verificado pela BTS, não sejam iguais (como observado na instanciação desses processos).
O resultado dessa composição é o processo Cell1_Cell2 (Fig. 5.7) que pode então ser
composto com Cell3.
Figura 5.8: Composição em interleave de Cell1, Cell2 e Cell3
Cell1_Cell2_Cell3 = Cell1_Cell2 [|||] Cell3
A composição desses componentes (Fig. 5.8) completam a composição das células em
nosso exemplo, as quais não têm comunicação entre si, mas apenas com o ambiente.
Communication
Em nosso exemplo do Buffer Circular, a composição em comunicação consiste em
verificar a interação entre os componentes, ou seja, essa regra faz a verificação da comunicação do Controller com as células e requer um conjunto de análise mais complexo. Na
ferramenta, compomos o Controller com o resultado da composição entre as três células
5.2 Aplicação do Buffer Circular na BTS
73
(Fig. 5.9). Nesse estudo de caso, realizamos a composição em comunicação com entre os
canais wrt_i.1 e write.1. A análise da composição entre esses componentes é realizada a
partir da comunicação entre esses dois canais.
Figura 5.9: Composição em Communication do Controller com as Células
Feedback
Na composição por feedback são selecionados dois canais do componente, gerado a
partir da composição entre o Controller e as células. Essa regra verifica se a comunicação
em um canal não interfere na comunicação do outro. Para nosso estudo de caso, realizamos
três composições em feedback: compomos os canais rd_i.1 e read.1 ; wrt_i.2 e write.2 ;
rd_i.2 e read.2.
Figura 5.10: Composição em feedback do componente resultante das células com o Controller
Reflexive
A última composição verificada é a reflexiva (Fig. 5.11) entre dois canais do componente resultante da composição em feedback. Essa regra verifica se existem problemas
5.3 Análise do Estudo de Caso
74
de dependência sobre a comunicação dos eventos no sistema. A composição foi realizada
entre os canais wrt_i.3 e write.3 ; rd_i.3 e read.3.
Figura 5.11: Composição em reflexive do componente resultante da composição em feedback
5.3
Análise do Estudo de Caso
Assim como descrito no processo original, nossa ferramenta foi capaz de gerar e verificar toda especificação do estudo de caso apresentado em [OLIVEIRA, 2012b]. Esse veio
validar nossa ferramenta, em relação a abordagem manual, quanto à facilidade, redução
da complexidade, tempo de resposta e confiabilidade.
Todo conjunto de regras e leis são definidos internamente pela ferramenta, de forma
automática, através de asserções FDR2. A tabela a seguir apresenta o conjunto de asserções gerado automaticamente em cada fase do estudo de caso. Os testes foram realizados
em uma máquina Pentium(R) Dual-Core CPU T4400 @ 2.20GHz, com 4Gb RAM e sistema operacional Ubuntu 12.04.
I/O process de Cell (3)
Asserções geradas e
Chamadas a proces-
Total de linhas no
verificadas
21
sos externos
48
script CSP
705
tempo de execução
2s07ms
I/O process de Controller (1)
9
16
261
14s.
Composições em Interleave (2)
2
4
508
1s8ms
Composição em
43
62
372
3s64ms
Composições em feedback (3)
135
192
1122
7m58s
Composições em reflexive (2)
88
132
782
4m77s
Total
298
454
3750
17m21s
communication (1)
Como podemos observar na tabela, cada coluna representa um uma fase de verificação,
como por exemplo, o resultado da verificação de I/O process das três celulas.
5.3 Análise do Estudo de Caso
75
Na primeira linha da tabela podemos observar a quantidade de asserções geradas e
verificadas. Ou seja, para a verificação de I/O process das três células, por exemplo, temos
a totalidade de 21 asserções geradas. Já as três composições em feedback totalizaram 135
asserções geradas automaticamente.
A BTS também inclui alguns arquivos externos que possuem a implementação de
processos usados na verificação das asserções, como descrito na segunda linha da tabela.
Esta representa a quantidade de chamadas a esses processos na execução dos arquivos
gerados. Além disso, a tabela apresenta a quantidade de linhas de código gerada e o
tempo de processamento em cada fase. Esse tempo foi medido manualmente e representa
desde o momento de solicitação para aquela verificação, até a apresentação do resultado
pela BTS ao usuário.
Uma das grandes contribuições da aplicação deste estudo de caso é a geração e verificação automática de 298 asserções de forma oculta ao usuário, além das 454 chamadas à
processos, que implementam as propriedades e regras descritas em [RAMOS, 2011], sendo
estas, através do FDR2, capazes de avaliar e validar a composição de componentes no
sistema. Além disso, os scripts CSP gerados em cada fase totalizaram 3750 linhas de
código.
76
6
Considerações finais
A automatização do processo de desenvolvimento de software é de extrema importância nos dias atuais, principalmente quando tratamos de características que são indispensáveis nesse processo, mas que requerem muito tempo e um alto custo.
Como dito anteriormente, o desenvolvimento de componentes tem ganhado destaque
nos últimos anos, devido à facilidade de manutenção, reutilização e confiabilidade, a
qual deve estar associada não só aos componentes, mas também à forma como esses são
compostos no sistema.
Em nosso trabalho propomos a implementação de uma ferramenta que faz uma verificação prévia da composição de forma automatizada. Esta implementa a abordagem
proposta em [RAMOS, 2011] que apresenta todas as verificações e validações através do
método formal CSP.
A abordagem foi baseada em um modelo de componentes e possui quatro formas de
composição. A composição é validada através da verificação de determinadas condições.
Uma vez satisfeitas as condições de aplicação da composição, a abordagem garante que o
sistema resultante é livre de deadlocks.
Iniciamos nosso trabalho com um estudo da abordagem utilizada. Logo em seguida,
visando um melhor entendimento e uma melhor aprofundamento no tema, fizemos uma
avaliação do estudo de caso proposto em [OLIVEIRA, 2012b] que aplica a abordagem a
um estudo de caso através do FDR2. A partir dessa análise, iniciamos a implementação de
nossa ferramenta utilizando a linguagem de programação Java e outras duas ferramentas
de apoio: o typeChecker e FDR2.
A ferramenta desenvolvida é capaz de, a partir da definição de um modelo de componente, verificar se sua comunicação com outros componentes é segura. Essa verificação
é feita através das características definidas pelo usuário, como comportamento, portas,
interface. Internamente a ferramenta gera arquivos CSP e realiza a verificação automaticamente. O resultado dessa verificação é transmitido diretamente para o usuário.
6.1 Trabalhos Futuros
77
Para avaliar nossa ferramenta realizamos um estudo de caso, onde geramos e testando
os componentes e sua composição a partir do exemplo clássico de buffer circular. Através
desse estudo de caso conseguimos avaliar características como redução da complexidade,
onde o usuário precisaria desenvolver e aplicar todas as regras e propriedades através da
linguagem CSP. Agora tudo é implementado internamente pela ferramenta e não é preciso
ter conhecimento sobre o FDR2.
A ferramenta apresenta ganho em relação a geração das condições de verificação automaticamente e a comunicação direta com o FDR2 sem conhecimento do usuário. Com
isso, abstraímos aos olhos do utilizador toda implementação das regras e propriedades
impostas em [RAMOS, 2011]. Porém, é necessário que o usuário tenha conhecimento
sobre a abordagem, para que, caso a BTS apresente alguma condição como inválida, seja
possível identificar o erro e consertar na descrição do modelo de componente.
6.1
Trabalhos Futuros
Nessa versão da ferramenta ainda não é possível ter um processo totalmente automatizado, por a descrição do comportamento do componente ser implementado manualmente.
Nesse contexto, como trabalhos futuros, pretende-se utilizar a plataforma Spoofax 1 , onde
é possível descrever linguagens como CSP utilizando um alto nível de formalismo, como
por exemplo, a linguagem de modelagem UML 2 . Com isso, temos a possibilidade de
omitir a linguagem CSP do usuário.
Ainda no trabalho de [RAMOS, 2011], foi proposto um estilo arquitetural chamado
BRICK. Nele, os contratos de componentes são enriquecidos com metadados que executam informações adicionais úteis na verificação da composição. Esses metadados da
composição são derivados dos metadados dos componentes que a constitui. Como trabalho futuro, pretendemos estender a BTS para o modelo de contrato de componente
enriquecido com metadados.
1
http://strategoxt.org/Spoofax/
2 http://www.uml.org/
78
Referências Bibliográficas
ABRIAL, J.-R. et al. Rodin: an open toolset for modelling and reasoning in event-b.
Int. J. Softw. Tools Technol. Transf., Springer-Verlag, Berlin, Heidelberg, v. 12, n. 6, p.
447–466, nov. 2010. ISSN 1433-2779. Disponível em: <http://dx.doi.org/10.1007/s10009010-0145-y>.
BARBOSA, D. Um Método Automático de Teste Funcional para a Verificação de Componentes. Dissertação (Mestrado) — Departamento de Computação - Universidade Federal
de Campina Grande, 2005.
BARN, B.; BROWN, A. W. Methods and tools for component based development. In:
Proceedings of the Technology of Object-Oriented Languages and Systems. Washington,
DC, USA: IEEE Computer Society, 1998. (TOOLS ’98), p. 384–. ISBN 0-8186-8482-8.
Disponível em: <http://dl.acm.org/citation.cfm?id=832254.832826>.
BERTOLINI, C.; MOTA, A. Ideas08: An strategy for automatic conformance testing in
embedded systems. Latin America Transactions, IEEE (Revista IEEE America Latina),
v. 6, n. 3, p. 290–297, 2008. ISSN 1548-0992.
BROWN, A. W.; SHORT, K. On components and objects: The foundations of componentbased development. In: Proceedings of the 5th International Symposium on Assessment
of Software Tools (SAST ’97). Washington, DC, USA: IEEE Computer Society, 1997.
(SAST ’97).
BROWN, A. W.; WALLNAU, K. C. The current state of cbse. IEEE Software, v. 15, n. 5,
p. 37–46, 1998.
BROWNLEE, N. Formal systems (europe) ltd. failures-divergence refinement. fdr2
user manual. available at http://www.formal.demon.co.uk/fdr2manual/index.html.
In:
Blount MetraTech Corp. Accounting Attributes and Record Formats
http://www.ietf.org/rfc/rfc2924.txt. [S.l.: s.n.], 2000.
CAVALCANTI, A.; GAUDEL, M.-C. Testing for refinement in csp. In: BUTLER, M.;
HINCHEY, M. G.; LARRONDO-PETRIE, M. M. (Ed.). Formal Methods and Software
Engineering, 9th International Conference on Formal Engineering Methods, ICFEM 2007,
Boca Raton, FL, USA, November 14-15, 2007, Proceedings. [S.l.]: Springer, 2007. (Lecture
Notes in Computer Science, v. 4789), p. 151–170. ISBN 978-3-540-76648-3.
CLARKE JR., E. M.; GRUMBERG, O.; PELED, D. A. Model checking. Cambridge, MA,
USA: MIT Press, 1999. ISBN 0-262-03270-8.
DIACONESCU, R.; FUTATSUGI, K. CafeOBJ report : the language, proof techniques,
and methodologies for object-oriented algebraic specification. Singapore, River Edge, NJ,
London: World scientific, 1998. (AMAST series in computing). ISBN 981-02-3513-5. Disponível em: <http://opac.inria.fr/record=b1104496>.
Referências Bibliográficas
79
EASSA, F. E.; ABULNAJA, O. A. Building uml-based use case sub-tool for componentbased software development. In: Proceedings of the ACS/IEEE International Conference
on Computer Systems and Applications. Washington, DC, USA: IEEE Computer Society,
2001. (AICCSA ’01), p. 454–. ISBN 0-7695-1165-1. Disponível em: <http://dl.acm.org/citation.cfm?id=872017.872219>.
FEITOSA, C.; PERES, G.; MOTA, A. Unifying models of test cases and requirements.
In: CIbSE. [S.l.: s.n.], 2008. p. 113–126.
GRIESKAMP, W. et al. Generating finite state machines from abstract state machines.
In: in Proceedings of International Symposium on Software Testing and Analysis (ISSTA.
[S.l.: s.n.], 2002.
GROOVER, M. P. Automation, Production Systems, and Computer-Integrated Manufacturing. 3rd. ed. Upper Saddle River, NJ, USA: Prentice Hall Press, 2007. ISBN
0132393212.
HOARE, C. A. R. Communicating sequential processes. Commun. ACM, ACM, New
York, NY, USA, v. 21, n. 8, p. 666–677, ago. 1978. ISSN 0001-0782. Disponível em:
<http://doi.acm.org/10.1145/359576.359585>.
HOARE, C. A. R. Communicating Sequential Processes. [S.l.]: Prentice-Hall, 1985. ISBN
0-13-153271-5.
ISOBE, Y.; ROGGENBACH, M. Webpage on CSP-Prover. http://staff.aist.go.
jp/y-isobe/CSP-Prover/CSP-Prover.html.
JOLLIFFE, G. Cost-efficient methods and processes for safety relevant embedded systems
(cesar) - an objective overview. In: SSS. [S.l.: s.n.], 2010. p. 37–50.
KICZALES, G. et al. Getting started with aspectj. Communications of the ACM, v. 44,
p. 59–65, 2001.
LAMPORT, L. The temporal logic of actions. ACM Trans. Program. Lang. Syst., ACM,
New York, NY, USA, v. 16, n. 3, p. 872–923, maio 1994. ISSN 0164-0925. Disponível em:
<http://doi.acm.org/10.1145/177492.177726>.
LAU, K.-K.; NTALAMAGKAS, I. Component-based construction of concurrent systems
with active components. In: Proc. 35th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA 2009). [S.l.]: IEEE, 2009. p. 497–502.
LAU, K.-K.; TAWEEL, F.; TRAN, C. The W Model for component-based software development. In: Proc. 37th EUROMICRO Conference on Software Engineering and Advanced
Applications. [S.l.]: IEEE, 2011. p. 47–50.
LAU, K.-K.; TRAN, C. M. X-man: An mde tool for component-based system development. 2010 36th EUROMICRO Conference on Software Engineering and Advanced
Applications, IEEE Computer Society, Los Alamitos, CA, USA, v. 0, p. 158–165, 2012.
LAU, K.-K.; Velasco Elizondo, P.; WANG, Z. Exogenous connectors for software components. In: Proc. 8th Int. SIGSOFT Symp. on Component-based Software Engineering,
LNCS 3489. [S.l.: s.n.], 2005. p. 90–106.
Referências Bibliográficas
80
LEDECZI, A. et al. The generic modeling environment. In: Workshop on Intelligent Signal
Processing. [S.l.: s.n.], 2001.
MARCILON, T. Contratos Formais para Derivação e Verificação de Componentes Paralelos. Dissertação (Mestrado) — Departamento de Computação - Universidade Federal do
Ceará, 2012.
MATSUMOTO, M.; FUTATSUGI, K. Highly reliable component-based software development by using algebraic behavioral specification. In: Proceedings of the 3rd IEEE International Conference on Formal Engineering Methods. Washington, DC, USA: IEEE Computer Society, 2000. (ICFEM ’00), p. 35–. ISBN 0-7695-0822-7. Disponível em: <http://dl.acm.org/citation.cfm?id=857176.857382>.
MATSUMOTO, M.; FUTATSUGI, K. The support tool for highly reliable componentbased software development. In: Software Engineering Conference, 2000. APSEC 2000.
Proceedings. Seventh Asia-Pacific. [S.l.: s.n.], 2000. p. 172–179.
MCILROY, M. D. Mass-produced software components. Proc. NATO Conf. on Software
Engineering, Garmisch, Germany, Springer-Verlag, 1968.
MOTA, A. et al. Evolving a safe system design iteratively. In: Proceedings of the 29th
international conference on Computer safety, reliability, and security. Berlin, Heidelberg:
Springer-Verlag, 2010. (SAFECOMP’10), p. 361–374. ISBN 3-642-15650-9, 978-3-64215650-2. Disponível em: <http://dl.acm.org/citation.cfm?id=1886301% -.1886337>.
NETO, E. Abordagem para Geração Automática de Código para Framework de Automação
de Testes. Dissertação (Mestrado) — Universidade Federal de Pernambuco, Centro de
Informática, 2007.
NIERSTRASZ, O.; DAMI, L. Component-Oriented Software Technology. 1995.
NIPKOW, T.; PAULSON, L. C.; WENZEL, M. Isabelle/HOL — A Proof Assistant for
Higher-Order Logic. [S.l.]: Springer, 2002. (LNCS, v. 2283).
NOGUEIRA, S.; SAMPAIO, A.; MOTA, A. Guided test generation from csp models.
In: FITZGERALD, J. S.; HAXTHAUSEN, A. E.; YENIGüN, H. (Ed.). ICTAC. [S.l.]:
Springer, 2008. (Lecture Notes in Computer Science, v. 5160), p. 258–273. ISBN 978-3540-85761-7.
OLIVEIRA, M. research report, An Exercise on Strong Output Decisiveness and Input
Determinism. Berlin, Germany: [s.n.], 2012.
OLIVEIRA, M. research report, Systematic Development of Constructive Componentbased Systems: a Quantitative Analysis. Berlin, Germany: [s.n.], 2012.
PERES, G.; MOTA, A. A tool to translate CSP models into english requirements. In: II
Encontro Brasileiro de Teste de Software. Recife: In: II Encontro Brasileiro de Teste de
Software, 2007.
PROBE User Manual. 2003. http://www.fsel.com/documentation/probe/
probe-doc-html/html/index.html.
Referências Bibliográficas
81
RAMOS, R. Systematic Development of Trustworthy Component-based Systems. Dissertação (Doutorado) — Universidade Federal de Pernambuco, Centro de Informática, 2011.
ROSCOE, A. W.; HOARE, C. A. R.; BIRD, R. The Theory and Practice of Concurrency.
Upper Saddle River, NJ, USA: Prentice Hall PTR, 1997. ISBN 0136744095.
RUMBAUGH, J.; JACOBSON, I.; BOOCH, G. Unified Modeling Language Reference
Manual, The (2nd Edition). [S.l.]: Pearson Higher Education, 2004. ISBN 0321245628.
SCHNEIDER, S. Concurrent and Real Time Systems: The CSP Approach. 1st. ed. New
York, NY, USA: John Wiley & Sons, Inc., 1999. ISBN 0471623733.
SCHNEIDER, S. The B-Method: An Introduction. [S.l.]: Palgrave Macmillan, 2001. (Cornerstones of Computing).
SMITH, G. The Object-Z Specification Language. [S.l.]: Kluwer Academic Publishers,
2000. 160 p.
SPAGNOLI, L. de A.; BECKER, K. UM ESTUDO SOBRE O DESENVOLVIMENTO
BASEADO EM COMPONENTES. [S.l.], Maio 2003.
STANKOVIC, J. A. et al. VEST: An Aspect-Based Composition Tool for Real-Time Systems. 2003.
SZYPERSKI, C. Component Software: Beyond Object-Oriented Programming. 2nd.
ed. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 2002. ISBN
0201745720.
VALLECILLO, A.; VASCONCELOS, V. T.; RAVARA, A. Typing the behavior of software components using session types. Fundam. Inf., IOS Press, Amsterdam, The Netherlands, The Netherlands, v. 73, n. 4, p. 583–598, set. 2006. ISSN 0169-2968. Disponível
em: <http://dl.acm.org/citation.cfm?id=1231191% -.1231198>.
VINCENZI, A. M. R. et al. Desenvolvimento baseado em componentes: Conceitos e
. [S.l.]: Editora Ciência Moderna Ltda., 2005. cap. Software Baseado
técnicas. In:
em Componentes: Uma Revisão sobre Teste.
WARMER, J.; KLEPPE, A. The Object Constraint Language: Getting Your Models Ready
for MDA. 2. ed. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 2003.
ISBN 0321179366.
WIRTH, N. A brief history of software engineering. IEEE Annals of the History of Computing, v. 30, n. 3, p. 32–39, 2008.
WOODCOCK, J. C. P.; CAVALCANTI, A. L. C. The semantics of circus. In: BERT, D.
et al. (Ed.). ZB 2002: Formal Specification and Development in Z and B. [S.l.]: SpringerVerlag, 2002. (Lecture Notes in Computer Science, v. 2272), p. 184—203.