Uma Metodologia para
Verificação de Modelos de
Sistemas de Comércio Eletrônico
Adriano Machado Pereira ([email protected])
Orientador: Wagner Meira Jr. ([email protected])
Co-orientador: Sérgio Campos ([email protected])
28 de Agosto de 2002
e-Commerce, Systems Performance Evaluation,
and Experimental Development Laboratory
Introdução
e -speed
• Comércio eletrônico (C.E.)
–
–
–
–
Popularização;
Usuários web mais exigentes;
Serviços cada vez mais complexos;
Difícil projeto.
• Processo de concepção de sistemas de
comércio eletrônico: maioria das abordagens
são ad-hoc
– Sistemas menos confiáveis;
– Alto custo.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
2
Introdução
e -speed
• Garantir a corretude de sistemas de
comercio eletrônico:
– Tarefa não trivial;
– Testes e Simulações são pouco eficientes.
• Qual a solução?
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
3
Metodologia CAFE
e -speed
• Níveis:
– Conceitual
– Aplicação
– Funcional
– Execução ou Arquitetural
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
4
e -speed
Metodologia CAFE
C
A
F
E
Entidades
Itens
Serviços
Arquitetura
Ciclo de Vida
Produtos
Ambiente de
Execução
Ações
Requisitos
Funcionais
Modelo de
Execução
Agentes
Estratégia de
Armazenamento
Ferramentas
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
Metodologia CAFE
e -speed
• Direcionada
para
concepção
sistemas de comércio eletrônico.
de
– Por que não adotá-la simplesmente?
• Quem projeta os sistemas?
• Quem produz os equipamentos de informática?
Ser humano
não é perfeito!
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
6
e -speed
Motivação
• Erros existentes nos sites são empecilhos
para um maior crescimento do comércio
eletrônico, pois podem trazer prejuízos para
os usuários web, site ou ambos, dependendo
de sua natureza;
• Processos de engenharia de software
voltados para sistemas genéricos (RUP,
Praxis);
• Ausência
de
metodologia
(grau
de
formalidade) específica para sistemas onde
há comercialização de bens.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
7
e -speed
Objetivo
• Elaborar uma metodologia que utiliza métodos
formais, mais especificamente verificação de
modelos, para projetar sistemas de comércio
eletrônico e verificar automaticamente se suas
regras de negócio são satisfeitas;
• Validar a metodologia através de estudos de
caso de comércio eletrônico.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
8
e -speed
Verificação de Modelos em
Sistemas De Comércio Eletrônico
• Regras de negócio
• Modelo formal de sistemas de comércio
eletrônico
– Propriedades
• Completeza
• Transitividade
• Suporte
Transacional
do
Transação
(Atomicidade,
Isolamento)
Servidor
de
Consistência,
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
9
e -speed
A Metodologia Formal-CAFE
• Baseada na metodologia CAFE de
especificação de sistemas de comércio
eletrônico;
• Estende a CAFE definindo método que
possibilita a verificação de modelos de
sistemas de comércio eletrônico;
• Incremental e dividida em 4 níveis.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
10
e -speed
A Metodologia Formal-CAFE
C
A
F
Regras
De
Negócio
Model.
Formal
Model.
Formal
Model.
Formal
Espec.
Formal
Espec.
Formal
Espec.
Formal
Verif.
Formal
Verif.
Formal
Verif.
Formal
Sistema Correto
E
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
11
A Metodologia Formal-CAFE
e -speed
• Conceitual:
– Tupla: < P, I, D, Ag, Ac, S > ;
– RegrasExplicação
de negócio;
dos níveis e
acompanhamento
através
um
– Quanto
mais detalhado
for,demelhor!
estudo de caso de uma Loja Virtual.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
12
e -speed
Estudo de Caso – Loja Virtual
Nível Conceitual
• Produto: livro;
• Itens: são unidades deste livro;
• Domínio:
não
disponível,
reservado, vendido, excluído;
• Agentes: comprador e vendedor;
• Ações:
disponível,
– Comprador:
Navegar,
Reservar,
Cancelar
Reserva, Comprar
– Vendedor: Disponibilizar, Excluir, Alterar
• Serviços: Efetuar reserva, Excluir produto,
etc.
13
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
Estudo de Caso – Loja Virtual
Nível Conceitual
e -speed
• Regras de negócio:
– Se um item está indisponível e a ação
Disponibilizar é executada sobre ele, então
o item deverá estar disponível no estado
seguinte.
– Se o item está reservado para um
comprador e este executa a ação comprar,
então o estado seguinte deste item será
vendido.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
14
Estudo de Caso – Loja Virtual
Nível Conceitual
e -speed
• Regras de negócios:
– Reservar um item e cancelar a reserva de
outro item do mesmo produto devem ser
serviços atômicos.
– Se o estoque é positivo, então deve
necessariamente existir pelo menos um
item no estado disponível.
– Etc.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
15
A Metodologia Formal-CAFE
e -speed
• Aplicação:
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
16
A Metodologia Formal-CAFE
• Aplicação:
e -speed
– ciclo de vida do bem comercializado (item);
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
17
Estudo de Caso – Loja Virtual
Nível Aplicação
e -speed
• Propriedade de Completeza
– EF (item1.estado = Indisponível)
– EF (item1.estado = Excluído)
item
– EF (comprador.ação = Reservar)
– EF (comprador.ação = Comprar)
comprador
– EF (vendedor.ação = Disponibilizar)
– EF (vendedor.ação = Excluir)
vendedor
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
18
A Metodologia Formal-CAFE
e -speed
• Funcional:
– Serviços providos pelo sistema;
– Múltiplos agentes;
– Múltiplos itens.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
19
Estudo de Caso – Loja Virtual
Nível Funcional
e -speed
• Propriedade de Transitividade
– AG (estado = Indisponível & serviço =
Disponibilizar)  AX (estado = Disponível)
– AG (estado = Disponível & serviço =
Excluir)  AX (estado = Excluído)
– AG (estado = Reservado & serviço =
Comprar)  AX (estado = Vendido)
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
20
Estudo de Caso – Loja Virtual
Nível Funcional
• Propriedades Transacionais
e -speed
– Atomicidade:
• Ex: Se um item está disponível e um
comprador tenta reservá-lo, o item deverá estar
reservado no próximo estado e o estoque
alterado ou então o estado deve ser mantido.
AG ((estado = Disponível & serviço = Reservar &
estoque = v)  AX ((estado = Disponível & estoque = v) |
(estado = Reservado & estoque = v – 1)))
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
21
Estudo de Caso – Loja Virtual
Nível Funcional
• Propriedades Transacionais
e -speed
– Isolamento:
• Ex: Se existirem dois compradores, um
reservando um item e outro cancelando a
reserva de outro item do mesmo produto, o
estoque do produto deve ser mantido
consistente.
AG ((serviço_comprador1 = Reservar &
serviço_comprador2 = Cancelar Reserva
& estoque = v)  AX (estoque = v))
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
22
Estudo de Caso – Loja Virtual
Nível Funcional
• Propriedades Transacionais
e -speed
– Consistência:
• Ex: o estoque de um determinado produto
nunca deve ser negativo.
AG !(estoque < 0)
• Ex: Se o estoque é positivo, então deve existir
pelo menos um item disponível.
AG ((estoque > 0)  (estado_produto = Disponível))
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
23
e -speed
Estudo de Caso – Loja Virtual
Nível Funcional
• Atomicidade e Isolamento evitam
inconsistência no sistema
• Erro grave detectado: violação da
propriedade
de
isolamento,
que
ocasionou que um mesmo item de um
produto fosse vendido duas vezes.
• Solução: mecanismo de exclusão
mútua no processo de reserva de itens.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
24
Estudo de Caso – Loja Virtual
Nível Funcional
• Erro detectado:
e -speed
next (em_uso) := case
...
next (sessão_usuário)
:= case
em_uso
= 0 & serviço comprador 1 = Reservar & serviço comprador 2 =
...
Reservar & estoque
> 0 & estoque
<= &
2 serviço
: {1,2}; comprador = Reservar &
Resultado:
sessão_usuário
= seleção
de produto
= 1 &disponível
serviço
comprador
1 = Cancelar
Reserva
: 0;a variável
next(produto
= 1)a: carrinho
de
– Quandoem_uso
um comprador
solicitar
reserva
decompras;
um item,
caso
em_uso
=1
serviço
comprador
1 = Comprar
0; então a=adição
sessão_usuário
= seleção
de
& serviço: comprador
Reservar
em_uso contenha
a &identificação
deproduto
outro
comprador,
do&
em_uso
= 2 & serviço comprador
2(“produto
= Cancelar
Reserva : 0;
next(produto
= 0)não
: erro
indisponível”);
item ao seu
carrinho disponível
de compras
é efetuada.
em_uso = 2 & serviço comprador 2 = Comprar : 0;
...
...
1: sessão_usuário;
1: em_uso;
esac;
esac;
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
e -speed
A Metodologia Formal-CAFE
– Execução ou Arquitetural:
– Componentes do sistema;
– Interações do usuário.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
26
e -speed
Estudo de Caso – Loja Virtual
Nível Execução / Arquitetural
• Verificação de todas as propriedades
verificadas nos níveis antecedentes.
• Novas especificações para verificar o
correto
funcionamento
dos
componentes da arquitetura do sistema.
• 71 especificações verificadas.
• Modelo completo: mais de 1023 estados,
com mais de 1014 estados alcançáveis.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
27
e -speed
Conclusão
• A aplicação de verificação de modelos em
comércio eletrônico tem se mostrado
promissora;
• Área pouco explorada;
• Processo de verificação em sistemas de
software não é trivial, porém a definição de
uma metodologia para tal é necessária e
tende a atrair pessoas para a área.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
28
Contribuições
e -speed
• Definição uma metodologia que possibilite:
– Identificar antecipadamente erros no projeto;
– Projetar sistemas de comércio eletrônico mais
confiáveis e robustos.
• Oportunidade de estender o trabalho a outras
áreas de aplicação;
• Demonstração que a aplicação de técnicas
formais pode ser útil e promissora.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
29
Publicações
e -speed
• ICFEM’02
– “A Formal Methodology to Specify e-Commerce
Systems”
• Artigo WMF’2002
– “Uma Metodologia para Verificação de Modelos de
Sistemas de Comércio Eletrônico”
• Artigo ICECR-5
– “Formal-CAFE Methodology:
System's Case Study”
an
E-commerce
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
30
e -speed
Trabalhos Futuros
• Definição de padrões para especificação
formal de regras de negócio de comércio
eletrônico (CE);
• Definição de padrões para construção do
modelo formal proposto pela metodologia;
• Definição de uma linguagem formal para
construção de sistemas de CE;
• Aplicação da metodologia em outras áreas,
tais como comércio eletrônico móvel e
telecomunicações.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
31