Instituto de Computação - Unicamp
O Sistema TeleMicro
Especificação e Validação
Marcelo Fantinato
Tarcisio da Rocha
Profa. Eliane Martins
Maio de 2002
O Projeto TeleMicro
 A proposta do sistema TeleMicro é dar a
seus usuários uma maior capacidade de
gerenciamento e acompanhamento de
suas ligações telefônicas realizadas a
partir de um microcomputador.
O Projeto TeleMicro
Pacotes
 Funcionalidades dividas em 3 pacotes:
Controle Telefônico
1. Efetuar Ligação
2. Receber Ligação
3. Programar Ligação Automática
Manutenção
1. Efetuar Login
2. Manter Cadastro de Operadoras
3. Cadastrar Nova Cidade
4. Manter Cadastro de Usuários
5. Alterar Perfil do Usuário
2. Manter Lista de Contatos
Consultas
1. Consultar Tarifas
2. Consultar Ligaçoes Realizadas
O Projeto TeleMicro
Pacote de Controle Telefônico
 Efetuar Ligação
Selecionar Operadora
<<include>>
<<extend>>
Selecionar Últimos Telefones
Discados
Usuário
Efetuar Ligação
<<extend>>
<<include>>
Selecionar Telefone de Contato
Acompanhar Ligação
O Projeto TeleMicro
Pacote de Controle Telefônico
 Receber Ligação
Chamador
Receber Ligação
<<include>>
Acompanhar Ligação
Usuário
O Projeto TeleMicro
O pacote de Controle Telefônico
 Programar Ligação Automática
<<extend>>
Usuário
Programar Ligação Automática
<<include>>
Verificar Ligações Automáticas a
Disparar
<<extend>>
Selecionar Operadora
Efetuar Ligação Automática
O Projeto TeleMicro
Diagrama de Classes
O Projeto TeleMicro
Diagrama de Classes
O Projeto TeleMicro
Diagrama de Classes
O Projeto TeleMicro
Diagrama de Classes
O Projeto TeleMicro
Outros Documentos
 Especificação Suplementar (Requisitos
Não Funcionais)
 Diagramas de Seqüência
 Dicionário de Dados
 Glossário
O Projeto TeleMicro
Especificação Formal
 Uso de Máquinas de Estados Finitos
Básicas
 Linguagem de especificação:
 Promela = Process Meta Language
 Ferramenta de Validação:
 Spin = Simple Promela Interpreter
 Visualizador Gráfico para Spin:
 XSpin
O Projeto TeleMicro
A Ferramenta Spin
 Apoio à verificação formal de sistemas.
 Enfoque em sistemas concorrentes.
 Análise da consistência lógica de uma
especificação.
 Deadlocks, livelocks, starvation, código
morto, violações...
 Permite o uso de assertivas.
 Permite simulação automática.
 Permite análise léxica
O Projeto TeleMicro
A Linguagem Promela
 Especificação de sistemas de estados
finitos.
 Parecida com a linguagem C.
 Modelo:





Declaração de Tipos
Declaração de Canais
Declaração de Variáveis
Declaração de Processos
O Processo Init
O Projeto TeleMicro
A Linguagem Promela
mtype = {MSG, ACK};
chan toS = ...
chan toR = ...
bool flag;
proctype Sender() { ...
}
proctype Receiver() { ...
}
init { ... }
Tipos
Canais
Variáveis
Processos
Init
O Projeto TeleMicro
A Linguagem Promela
mtype = { RED, YELLOW, GREEN } ;
proctype SinalDeTransito() {
byte state = GREEN;
do
:: (state == GREEN) -> state = YELLOW;
:: (state == YELLOW)-> state = RED;
:: (state == RED)
-> state = GREEN;
od;
}
init { run SinalDeTransito() }
O Projeto TeleMicro
A Linguagem Promela
mtype = { RED, YELLOW, GREEN } ;
proctype SinalNaoDetermimistico(){
byte state = GREEN;
do
:: state = YELLOW;
:: state = RED;
:: state = GREEN;
od;
}
init { run SinalDeTransito() }
O Projeto TeleMicro
Modelando o Controle Telefônico
Controle Telefônico
1. Efetuar Ligação
2. Receber Ligação
3. Programar Ligação Automática
 Pacote principal do sistema
 Compartilham recursos únicos (modem)
 Complementar os outros modelos
Imposs ível
Realizar Lig
Operadora Não
Cadastrada
Inf. No.
Manualmente
Es c. No. pela
Lis ta de Contatos
Dis cando
Atual. Lista de Últimos
Nos. Disc ados
Selec ionar a
Operadora
Reg. Dados
da Lig
Inf. No. de
Telelefone
Es c. pelos últimos
Nos. dis cados
Ac ompanhar
Ligaç ão
Aguardar Atend.
da Lig. "a Cobrar"
Ident. Tipo
de Ligação
Definir
Operaç ão
Enviar Ms g.
Padrão
Apres. No. do
Chamador
Apresentar Nome do
Chamador
Aguardar Atend. da
Lig. não "a Cobrar"
Atender a
Lig. Automat.
Inf. No.
Manualmente (P)
Inf. No. de
Telelefone (P)
Operadora não
Cadastrada (P)
Es c. No. pela Lista
de Contatos (P)
Es c. pelos últimos
Nos. dis cados (P)
Enviar Ms g.
Personal.
Inf. Data e Hora
a s er Real.
Selec ionar
Mens agem
Inc . a Lig.
Aut. na Lis ta
Selec ionar
Operadora (P)
Ex ec . o Verif.
de Lig. Aut.
Receber Ligação
Aguardando
Apres. Nome
22
Apres. número
24
23
25
Indet. Ligação
26 27
28
Lig a Cobrar
21
Lig Normal
29
31
Atender Autom.
30
Acomp. Lig
32
33
Msg Padrao
34
35
Reg Dados
Msg Person
36
O Projeto TeleMicro
Modelando o Controle Telefônico
 Análise Léxica
 Simulação
 Verificação
O Projeto TeleMicro
Conclusões
 Os modelos usados cobriram aspectos
complementares.
 O Modelo de Estados oferece uma descrição
global do comportamento do sistema, que não é
oferecida pelo Diagrama de Casos de Uso.
 O Modelo de Casos de Uso foi muito
importante para a modelagem de estados.
O Projeto TeleMicro
Conclusões
 Simulação e Verificação: possibilita a
identificação de inconsistências:
 no próprio modelo de estados, e
 em outros modelos, como o de casos de uso.
 O Potencial da ferramenta SPIN não foi
totalmente usado, pois o modelo de estados
básico é bem limitado.
 Percebeu-se que usando uma MEF Estendida,
o Modelo de Estados seria menor e mais
simples.
O Projeto TeleMicro
Conclusões
 Grandes benefícios ao Teste de Sistemas:
 Os cenários de uso do sistema podem ser facilmente
obtidos a partir do Modelo de Estados;
 Pode-se facilmente definir os casos de teste para
cada cenário (caminho a percorrer no modelo,
estado final esperado).
 Outros que serão cobertos em fase futura.
O Projeto TeleMicro
Referências Bibliográficas
 GILL, A., Introduction to the Theory of FSM. NY,
McGraw-Hill, 1962.
 PROMELA – Laguage Reference. Disponível em:
http://cm.bell-labs.com/cm/cs/what/spin/Man/promela.htm
 SPIN – Formal Verification. Disponível em: http://cm.belllabs.com/cm/cs/what/spin/
 OFFUTT, A. J.; LIU, S. E ABDURAZIK, A. Generating
Test Data From State-Based Specifications. JSTVR, 2000.
 Apfelbaum, L. e Meyer, S., Use Cases Are Not
Requirements. Disponível em: http://www.model-basedtesting.org