A Model Checking Methodology
for E-commerce Systems
Adriano Machado Pereira ([email protected])
Orientador: Wagner Meira Jr. ([email protected])
Co-orientador: Sérgio Campos ([email protected])
Universidade Federal de Minas Gerais
Departamento de Ciência da Computação
5 de agosto de 2003
e-Commerce, Systems Performance Evaluation,
and Experimental Development Laboratory
Introdução
e-speed
• Comércio eletrônico
–
–
–
–
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
e-speed
Introdução
• Garantir a corretude de sistemas de comércio
eletrônico:
– Tarefa não trivial;
– Testes e simulações são pouco eficientes.
• Qual a solução?
– Metodologia específica (CAFE);
– Uso de métodos formais.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
3
e-speed
Motivação / Problema
• 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 de
comércio eletrônico.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
4
e-speed
Solução Proposta
• Elaboração de 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;
• Validação da metodologia através de estudos
de caso de comércio eletrônico.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
5
e-speed
Metodologia Empregada
• Baseia-se na metodologia CAFE de
especificação de sistemas de comércio
eletrônico;
• Utiliza métodos formais;
• Estende a CAFE definindo um 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
6
e-speed
Metodologia Empregada
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
7
Metodologia Empregada
e-speed
• Estudo de caso: Livraria virtual
• 71 propriedades verificadas;
• Modelo com mais de 1023 estados.
• Tipos de erros observados:
– Completeza do modelo;
– Transitividade;
– Suporte
transacional
Consistência, Isolamento).
(Atomicidade,
• Outro estudo de caso: leilão eletrônico.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
8
e-speed
Contribuições
• Definição
possibilita:
de
uma
metodologia
que
– 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
9
e-speed
Conclusão /
Originalidade do Tema
• Área pouco explorada;
• A aplicação de verificação de modelos em
comércio eletrônico tem se mostrado
promissora;
• 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
10
Publicações
e-speed
• SBC WMF’02 (Gramado – RS – Brasil)
– “Uma Metodologia para Verificação de
Modelos de Sistemas de Comércio Eletrônico”
• IEEE ICFEM’02 (Shanghai – China)
– “A Formal Methodology
Commerce Systems”
to
Specify
e-
• ICECR-5 (Montreal – Canada)
– “Formal-CAFE Methodology: an E-commerce
System's Case Study”
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
11
Publicações
e-speed
• EBR’02 (Rio de Janeiro – Brasil)
– “Model Checking Patterns for e-Commerce
Systems”
• Electronic Commerce Research
(Kluwer - Submetido em Dez/2002)
Journal
– “The Formal-CAFE Methodology and Model
Checking Patterns in the Specification of Ecommerce Systems”
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
12
Trabalhos Posteriores
e-speed
• Concluído:
– Definição de padrões para especificação formal
de regras de negócio de comércio eletrônico;
– Definição de padrões para construção do modelo
formal proposto pela metodologia;
• Em andamento:
– Definição de um processo unificado, que utilize a
metodologia Formal-CAFE e a linguagem UML
(Processo UML-CAFE);
– Utilização de SPE (Software Performance
Engineering) para sistemas de comércio
eletrônico.
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory
13
e-speed
Comentários, Críticas e
Perguntas?
e-Commerce, Systems Performance Evaluation, and Experimental Development Laboratory