O Sistema TeleMicro

Marcelo FantinatoTarcisio da Rocha

Profa. Eliane MartinsMaio de 2002

Instituto de Computação - Unicamp

Especificação e ValidaçãoEspecificação e Validação

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ção2. Receber Ligação3. Programar Ligação Automática

Consultas

1. Consultar Tarifas2. Consultar Ligaçoes Realizadas

Manutenção1. Efetuar Login2. Manter Cadastro de Operadoras3. Cadastrar Nova Cidade4. Manter Cadastro de Usuários5. Alterar Perfil do Usuário2. Manter Lista de Contatos

O Projeto TeleMicro

Pacote de Controle Telefônico Efetuar Ligação

Usuário

Selecionar Telefone de Contato

Selecionar Operadora

Acompanhar Ligação

Efetuar Ligação

<<include>>

<<include>>

Selecionar Últimos Telefones Discados

<<extend>>

<<extend>>

Receber Ligação

O Projeto TeleMicro

Pacote de Controle Telefônico

Chamador UsuárioReceber Ligação

Acompanhar Ligação

<<include>>

Programar Ligação Automática

O Projeto TeleMicro

O pacote de Controle Telefônico

Efetuar Ligação Automática

Usuário Verificar Ligações Automáticas a Disparar

Programar Ligação Automática

Selecionar Operadora

<<include>>

<<extend>>

<<extend>>

O Projeto TeleMicro

Diagrama de ClassesOperadora

CodOperadora : StringNome : String

CidadeCodCidade : StringNomeCidade : StringEstadoCidade : StringEhNacional : boolean

TarifaTarifa1Tarifa2Tarifa3Tarifa4Tarifa5Tarifa6Tarifa7Tarifa8TarifaSb1TarifaSb2TarifaSb3TarifaSb4TarifaDom1TarifaDom2

*

*

*

*

O Projeto TeleMicro

Diagrama de Classes

Ligacao EfetuadaValorLigacao : RealNumTelefone : StringTipoLigacao : String

EfetuarLigacao()

Ligacao RecebidaNumChamador : StringTipoLigacao : String

ReceberLigacao()

Ligacao a CobrarValorLigacao : Real

LigacaoDataLigacao : DateHoraLigacao : HoraDuracaoLigacao : Integer

AcompanharLigacao()FinalizarLigacao()

O Projeto TeleMicro

Diagrama de ClassesLigação AutomáticaNumTelefone : StringCodCidade : StringCodOperadora : StringDataLigacao : DataHoraLigacao : HoraMensagem : AudioEhNacional : boolean

UsuarioIdentUsuario : StringNomeUsuario : StringSenhaUsuario : StringTipoUsuario : String

ContatoNomeContato : StringSobrenomeContato : StringCargoContato : StringEmailContato : StringMsgContato : String

TelefoneNumTelefone : StringCodCidade : String

PerfilOperadoraPadrao : StringOpcaoOperadora : StringMsgPadrao : StringTipoSinal : StringNumChamadas : Integer

* 1

1

1* 1

1

*

1

*

**1

11 1

O Projeto TeleMicro

Diagrama de Classes

OperadoraCodOperadora : StringNome : String

CidadeCodCidade : StringNomeCidade : StringEstadoCidade : StringEhNacional : boolean

*

*

*

*

Ligacao EfetuadaValorLigacao : RealNumTelefone : StringTipoLigacao : String

EfetuarLigacao()

Ligacao RecebidaNumChamador : StringTipoLigacao : String

ReceberLigacao()

Ligacao a CobrarValorLigacao : Real

TarifaTarifa1Tarifa2Tarifa3Tarifa4Tarifa5Tarifa6Tarifa7Tarifa8TarifaSb1TarifaSb2TarifaSb3TarifaSb4TarifaDom1TarifaDom2

Lista de Ligacoes

ConsultarLigacoes()Incluir Ligação()

Programa de Ligações Automáticas

IncluirLigacao()VerificarLigacoesaDisparar()

LigacaoDataLigacao : DateHoraLigacao : HoraDuracaoLigacao : Integer

AcompanharLigacao()FinalizarLigacao()

*1 *1

1

*

1

*Perfil

OperadoraPadrao : StringOpcaoOperadora : StringMsgPadrao : StringTipoSinal : StringNumChamadas : Integer

Ligação AutomáticaNumTelefone : StringCodCidade : StringCodOperadora : StringDataLigacao : DataHoraLigacao : HoraMensagem : AudioEhNacional : boolean

* 1* 1

UsuarioIdentUsuario : StringNomeUsuario : StringSenhaUsuario : StringTipoUsuario : String

* 1* 1 1 11 1

*1*1

ContatoNomeContato : StringSobrenomeContato : StringCargoContato : StringEmailContato : StringMsgContato : String

1

*

1

*

TelefoneNumTelefone : StringCodCidade : String

*

1

*

1

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 Promelamtype = {MSG, ACK}; chan toS = ... chan toR = ... bool flag;proctype Sender()

{ ... }proctype Receiver() {

... }init { ... }

Tipos

Canais

Variáveis

Processos

Init

O Projeto TeleMicro

A Linguagem Promelamtype = { 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 Promelamtype = { 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ção2. Receber Ligação3. Programar Ligação Automática

Pacote principal do sistema Compartilham recursos únicos

(modem) Complementar os outros modelos

Inf. No. de Telelefone

Inf. No. Manualmente

Esc. No. pela Lis ta de Contatos

Operadora Não Cadastrada

Selec ionar a Operadora

Esc. pelos últimos Nos. discados

Discando

Impossível Realizar Lig

Definir Operação

Atual. Lista de Últimos Nos. Discados

Apres. No. do Chamador

Ident. Tipo de Ligação

Apresentar Nome do Chamador

Aguardar Atend. da Lig. "a Cobrar"

Aguardar Atend. da Lig. não "a Cobrar"

Atender a Lig. Automat.

Enviar Msg. Padrão

Enviar Msg. Personal.

Acompanhar Ligação

Reg. Dados da Lig

Inf. No. de Telelefone (P)

Inf. No. Manualmente (P)

Esc. No. pela Lista de Contatos (P)

Esc. pelos últimos Nos. discados (P)

Operadora não Cadastrada (P)

Selec ionar Operadora (P)

Inf. Data e Hora a ser Real.

Selec ionar Mensagem

Inc. a Lig. Aut. na Lis ta

Exec. o Verif. de Lig. Aut.

Aguardando Apres. número

Apres. Nome Indet. Ligação

Lig a Cobrar Lig Normal

Acomp. Lig

Atender Autom.

Msg Padrao Msg Person

Reg Dados

Receber Ligação

22

232425

26 2731

29 30 32 33

363534

21

28

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.bell-labs.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-based-testing.org