Testes de Sistemas Concorrentes:
Uma abordagem formal
Testing Concurrent Systems: A Formal Approach
Jan Tretmans – University of Twente
Paulo Eduardo e Silva Barbosa
Março de 2004
Introdução
Ultimamente
muita pesquisa foi dedicada à área
de métodos formais
A prática corrente de checagem de corretude é
baseada em uma abordagem mais informal
A combinação de testes e métodos formais nem
sempre é feita
Introdução
Pouca gente
imagina como uma mão lava a
outra
As
mãos sujas dos testes
A mão limpa e matemática dos métodos de
verificação formal
Introdução
As
visões estão mudando
Pesquisas acadêmicas com testes estão
evoluindo e mesmo o verificador mais formal
admite que um sistema verificado formalmente
ainda deve ser testado
Métodos formais são cada vez mais usados, uma
especificação formal pode ser benéfica durante
um teste, dando-lhe maior suporte
Propósitos
Discutir como testes podem ser
executados
baseados em especificações formais
Como obter vantagens em termos de precisão,
claridade e consistência do processo de testes
pela adoção de uma abordagem formal
Tópicos da discussão
Casamento entre
métodos formais e testes
A necessidade de ambos
Uma especificação formal verificada é um bom ponto
de partida para testes
Testes formais são um bom ponto de partida para
introduzir métodos formais no desenvolvimento de
software
Estrutura da apresentação
 Discussão
informal sobre testes de software clássicos
 Apresentação de um framework geral e formal para testes
utilizando métodos formais
 Faz uma discussão mais específica desse framework com o
formalismo dos sistemas de transições rotulados
 Discutimos o suporte ferramental e apresentamos um
exemplo de aplicação
 Discussão de fontes e perspectivas
Discussão informal sobre testes
de software clássicos
Testes de software
Apresentação da
abordagem clássica
A especificação é a base do teste
Ordens dos testes
Testes podem ser aplicados em diferentes níveis
de abstração
Teste
black-box ou funcional
Teste white-box
Teste grey-box
Fases do processo de testes
Geração dos
testes
Execução dos testes
Outras atividades importantes:
Gerenciamento
Manutenção
Automação dos testes
Teste é
um candidato ideal para automação
Ferramentas record and playback
Ferramentas de cobertura de código
Critérios:
 Todos
os caminhos
 Todos os statements
 Todas as combinações de uso
Framework para testes formais
Framework para testes formais
É apresentado um
framework para uso de métodos
formais em testes de conformidade
Testa com relação à sua especificação formal do seu
comportamento funcional
O mais importante é que liga o mundo informal das
implementações, testes e experimentações com o
mundo formal das especificações e modelos
Conceitos abordados no framework
Conformidade
Observações e
testes
Testes de conformidade
Suas extensões
Conformidade
 Necessitamos
de implementações e especificações
 As especificações são formais. Universo de
especificações é denotado por SPECS
 Implementações são os sistemas que iremos testar.
Denotamos por IUT pertencentes a IMPS
 IUT conforms-to s expressa que IUT é uma correta
implementação da especificação s.
 Formalmente sobre implementações, uma
implementação IUT  IMPS pode ser modelado
por um objeto formal Iiut  MODS
 Isso é chamado como hipóteses de teste
Hipóteses de teste
 Expressam
conformidade por uma relação formal entre
modelos de implementações e especificações
 IUT  IMPS é dita correta com relação a s 
SPECS, IUT conforms-to s, sss Iiut  MODS
de IUT é imp-relacionado com s: Iiut imp s.
 Uma relação de implementação
 imp
 MODS X SPECS
Observações e Testes
O comportamento de
uma IUT é investigado
fazendo experimentos na implementação e
observando as suas reações
casos de testes e execução de testes
Casos de testes e execução de
testes
 Considere
casos de testes formalmente pertencentes a um
domínio TESTS
 Requer um procedimento para executar um caso de teste t a
uma IUT
 Denotada por EXEC(t,IUT)
 O que acontece durante a execução
 A execução de um teste irá levar em um conjunto de
observações, subconjunto de OBS
 Função de observação:
 Obs:
TESTS X MODS  P(OBS)
 obs(t,Iiut) formalmente modela a execução do teste real EXEC(t,IUT)
Hipóteses de Testes
 Seu
significado:
 Para
todas as implementações reais que estamos
testando, assume-se que existe um modelo, tal que se
colocássemos a IUT e o modelo em black boxes e
fizéssemos todos os experimentos possíveis em
TESTS, não conseguiríamos distinguir entre a real IUT
e o modelo
Funções de veredito vt
 Usualmente
interpretamos observações de testes em
termos de certo ou errado
 Vt: P(OBS)  {fail, pass}
 Isso
 Uma
é extendido como uma suíte de testes:
implementação falha em uma suíte de testes se ela
não passa:
Testes de conformidade
Envolve saber se
uma implementação está
conforme respeito a uma relação de
implementação imp com sua especificação
Uma
suíte de testes com essa propriedade é
chamada completa
Pode
distinguir entre as implementações
conformes e não-conformes
É um requerimento muito forte para Testes
práticos
Implicações sound
Implicações exhaustiveness
Mostrar soundness
Se
a propriedade de completude for provada no nível
dos modelos, e se tivermos base que as hipóteses de
testes valem, então a conformidade de uma
implementação com respeito a sua especificação pode
ser decidida por meio de um procedimento de testes
Derivação de testes
Então, uma
atividade importante passa a ser
dividir os algoritmos no qual produzem suítes de
testes sound e/ou completos de uma
especificação dada uma relação de
implementação
Deve
produzir suítes de testes sound para
alguma especificação s
Extensões
Arquitetura de
testes: define o ambiente no qual
uma implementação é testada
Introdução da técnica de cobertura: a cada
implementação errônea detectada por uma suíte
de testes, é atribuido um valor e depois esses
valores são integrados
Sistemas de transição rotulados
De
que consiste
Seu formalismo modela comportamento de processos
(especificações, implementações e testes)
Serve como modelo semântico para várias linguagens
formais
Sistemas de transição rotulados
Os domínios formais SPECS, MODS
e TESTS serão
agora algum tipo de sistema de transição
Sua teoria de testes não serve para testes de
conformidade
Em vez de começar com uma especificação e encontrar
uma suíte de testes, define relações de implementação
Exemplo
 Dada
uma classe de testes:
 Um sistema de transição p é equivalente a um q se algum
caso de teste em uma classe leva às mesmas observações
com p e q
 Uma
vez que as relações de implementação tenham sido
definidas, o teste de conformidade inclui encontrar o
algoritmo de derivação de testes em que as suítes de testes
possam ser derivadas de uma especificação que sejam
sound e tentem ser mínimos
Teoria ioco-testing
Usa
os dois tipos de testes
Sua relação de implementação é definida como no slide
anterior
Derivação de testes a partir de especificações é feito do
resultado de um algoritmo de derivação de testes sound
ou exaustivo
Especificações
Utilizamos sistemas de
transições rotulados ou alguma
linguagem formal com a semântica de sistemas de
transições rotulados
Devemos conhecer as ações do sistema de transição e
deve ser particionado em entradas e saídas (Li e Lu)
LTS(L) – sobre ação do alfabeto L
SPECS := LTS(Li U Lu)
Implementações e seus modelos
Implementações são modeladas
por uma classe
especial de sistemas de transição chamados
input-output transition systems (IOTS)
IOTS(Li, Lu) classe com entradas Li e saída Lu
MODS := IOTS(Li, Lu)
IMPS são os programas que podem ser
modelados por IOTS
Relação de implementação
⊆ IOTS(Li,Lu) X LTS(Li U Lu)
 Observação de refutação  ∉ L
 TESTS = LTS(L U {})
 Enquanto observando um processo, uma
transição rotulada com  só pode ocorrer se
nenhuma outra é possível
 O observador sabe que o processo não pode
executar nenhuma das ações que ele oferece
 ioco
Operador paralelo
É
o tradicional operador paralelo de
sincronização extendido com a regra 
É
chamado refutação em pré-ordem
Relação de implementação mais
fraca (conf)
É
uma modificação do teste em pré-ordem
restringindo todas as observações para os traces
que estão contidos na especificação s
Facilita os testes porque deixa de considerar o
vasto conjunto complementar
Faz apenas o que deve fazer
A teoria dos testes canônicos baseia-se nessa
abordagem
Teste em pré-ordem para autômatos
entrada/saída
É
requisitado que as entradas estejam sempre
habilitadas
Relação ioco
Segue
os princípios dos testes em pré-ordem
com testes que possam refutar ações na
refutação em pré-ordem
Entradas estão sempre habilitadas
A distinção com o IOA é a restrição dos traces
apenas das especificações como em conf
Definição semi-formal da
relação ioco
p
after σ é o conjunto de estados onde o sistema
de transições p pode após executar o trace σ
out(p after σ) é o conjunto de ações de saída
após p after σ
Um estado p é quiescente se não pode ocorrer
ação de saída
Uma
ação δ, indicando quiescencia deve ocorrer
apenas se existe um estado quiescente em p
after σ
Straces(s) são traces de suspensão da
especificação, onde δ vai ocorrer com entradas e
saídas normais
 A relação
de implementação escolhida é a ioco: imp :=
ioco
 Uma implementação é ioco-correta com respeito a
especificação s se i nunca produz uma saída na qual
não poderia ser produzida por s na mesma situação,
após o mesmo trace de suspensão
 Então i deve ser apenas quiescente, não produzir saídas
se s for também
Exemplo 1
Exemplo 1
Dois
IOTS com Li = {?but} e Lu{!liq,!choc}
not( r1 ioco r2) pois:
out(r1 after ?but δ ?but) = {!liq, !choc},
Enquanto out (r2 after ?but δ ?but) = {!choc}
Testes
TESTS é
instanciado também com sistemas de
transições, mas adicionamos um rótulo extra θ
para detecção de refutação
Retringimos testes para sistemas determinísticos
com comportamento finito
Os estados terminais são pass ou fail
Testes
Para
cada estado não-terminal s de um test case que
init(s) = {a} para algum a ∈ Li, ou init = Lu U {θ}
init(t) é o conjunto de ações iniciais de t
O comportamento de cada test case é descrito por
uma árvore finita
O rótulo especial θ ∉ L U {δ} será usado para
detectar estados quiescentes de uma implementação
Normalmente é um tipo de time-out
Exemplo 2
Observações
São
logs de ações, traces sobre L U {θ}
OBS := (L U {θ})*
Função de observação: Composição
sincronizada paralela de t e i terminando em um
estado final de t
Exemplo 3
Para
r1 temos três observações com t do
exemplo 2:
Vereditos
atribuído a um conjunto de observações O 
OBS é pass se todos os traces em O leva ao
estado terminal pass do test case
É
Exemplo 4
No
exemplo 3, como o estado terminal de t para
a segunda vez é fail, o veredito de r1 é fail.
O veredito de r2 é pass
Execução de testes
EXEC(t, IUT) deve
expressar a semântica
expressa por obs(t, Iiut) e estabelece as
hipóteses de testes
Derivação de testes
 Algoritmo
que especifica a derivação dos test cases de
uma especificação de um sistema de transição rotulado
para a relação de implementação ioco
 “;” denota um prefixo de ação
 “+” denota escolha
 “” denota escolha generalizada
 S after a denota o conjunto de estados que podem ser
alcançados de algum estado em S via uma ação a
Algoritmo derivação de testes
ioco
Seja
s uma especificação com estado inicial s0
S é um conjunto não-vazio de estados com
inicialmente S = {s0}
Um test case t é obtido de S por um número finito
de recursões de uma das três escolhas nãodeterminísticas
Algoritmo derivação de testes
ioco
Sobre o algoritmo
uma especificação s  LTS(L1 U L2)
É provado que este algoritmo produz apenas
casos de testes sound (que nunca produzem fail
enquanto testando uma implementação iococonforming
Formalmente, seja der alguma função
satisfazendo o algoritmo não-determinístico,
então:
Dada
Alguma implementação não-conforme pode
ser
sempre detectada por caso de teste gerado por
esse algoritmo
Seja Ts o conjunto de todos os casos de testes
que podem ser gerados pelo algoritmo de s,
então:
Exemplo 5
Usando
o algoritmo de derivação ioco-test, o caso de
teste t da figura 2 pode ser derivado da especificação
r2 na figura 1
Isso é consistente com a figura 1 e exemplo 4:
R1 not ioco r2, r2 ioco r2 (reflexiva) e vt(obs(t,r1)) = fail
e vt(obs(t,r2)) = pass
O caso de teste t foi usado para detectar que r1 não é
ioco-correct com respeito a r2