Tópicos em Engenharia de
Software II
Fernando Castor
Profa.: Eliane Martins
1
Roteiro




Introdução e Objetivos
Técnica 1: Cálculo de Refinamentos
Técnica 2: Árvore de Falhas
Conclusões
2
Roteiro




Introdução e Objetivos
Técnica 1: Cálculo de Refinamentos
Técnica 2: Árvore de Falhas
Conclusões
3
Introdução



Nos dias atuais, sistemas de software
são empregados em praticamente todos
os ramos de nossa sociedade
Complexidade desses sistemas aumenta
a cada dia
Cada vez mais, requisitos de
dependability são exigidos
4
Introdução (cont.)

Dependability envolve diversos fatores:




Confiabilidade (reliability)
Segurança contra acidentes (safety)
Disponibilidade (availability)
Segurança contra intrusão (security)
5
Introdução (cont.)

Dependability envolve diversos fatores:




Confiabilidade (reliability)
Segurança contra acidentes (safety)
Disponibilidade (availability)
Segurança contra intrusão (security)
6
Confiabilidade
“The probability that a system will perform its
intended function for a specified period of
time under a set of specified environmental
conditions”
Nancy G. Leveson
Um sistema é confiável se ele se comporta
de acordo com sua especificação
7
Objetivos

Apresentar uma técnica para assegurar
confiabilidade e outra para analisar segurança
contra acidentes



Através de uma mesma aplicação exemplo:
algoritmo BubbleSort
A segunda técnica será usada para analisar a
confiabilidade do exemplo, devido à sua
simplicidade
Ressaltar as vantagens e desvantagens de
cada técnica, com relação ao estudo de caso
8
Roteiro




Introdução e Objetivos
Técnica 1: Cálculo de Refinamentos
Técnica 2: Árvore de Falhas
Conclusões
9
Refinamento


Se um programa prog2 é melhor que
um programa prog1, dizemos que prog2
refina prog1, ou prog1 prog2
Exemplos:


Algoritmos de ordenação: inteiros e
números de ponto flutuante ou apenas
inteiros?
Altímetro de um avião: faixa de valores ou
valor preciso?
10
Cálculo de Refinamentos

Conjunto de leis que visam produzir
programas confiáveis a partir de uma
especificação formal



Código produzido através do uso dessas leis
garantidamente implementa a especificação
Baseado no cálculo de predicados
Especificações são programas que não podem
ser executados por um computador:
x :[pre, pos]

Programas executáveis = código
11
Refinamento de Programas

Exemplo:
x:[ x > 0 ^ x|2, x > 100]
x:[ x > 0, x = 101]
ou
x:[x > 100 ^ x < 120]
Pré-condições são enfraquecidas
Pós-condições são fortalecidas
12
Algoritmo BubbleSort
m := #as;
do !(m = 0) {
n := 0;
do !(n = m – 1) {
if(as[n] > as[n+1]) {
swap(as[n], as[n+1])
}
else {
skip
}
n := n + 1
};
m := m - 1
}
13
Especificação do BubbleSort
var as:seqNZ; con A;
and A = bag as
as:[ i, j : 0 # as  i  j  as[i]  as[ j ] ]
14
Refinamento
(1)
post  i, j : 0 # as  i  j  as[i ]  as[ j ]
var as :seq N Ζ; con A; and A  bag as 
as : [ post]
 6.1
| [varn, m : N; and n  # as n  m  m  # as 
m, n, as[ post]
]|
15
Refinamento
(2)
 3 .3
INV1  (i, j : m  # as  i  j  as[i ]  as[ j ])
 (m  # as  l : 0  m  as[m]  as[l ])
m, n, as : [ INV1 ];
m, n, as : [ INV1 , post]
 1. 3
m : # as
Obrigação de P rova: pre  pos[m \# as]
16
Refinamento
(3)
 5 .1
m, n, as : [ INV1 , INV1  m  0];
Obrigação de P rova:
pre[m, n, as \ m0 , n0 , as0 ]  pos'  pos
 5 .5
do m  0 
m, n, as : [m  0  INV1 , INV1  0  m  m0 ];
od
17
Código resultante:
m :# as;
do m  0 
n : 0;
do n  m  1 
if(as[n]  as[n  1]) 
swap(as[n], as[n  1])
as[n]  as[n  1] 
skip
fi;
n : n 1
od
m : m  1
od
18
Características da Técnica

Vantagens:


O código gerado garantidamente atende à
especificação
Desvantagens:


Trabalho muito grande é necessário para
realizar o refinamento
Não garante a corretude da especificação
19
Roteiro




Introdução e Objetivos
Técnica 1: Cálculo de Refinamentos
Técnica 2: Árvore de Falhas
Conclusões
20
Algoritmo BubbleSort (versão implementada)
int m = as.length-1;
int n = 0;
while(0<m) {
while(n<m) {
if(as[n] > as[n+1]) {
int t = as[n+1];
as[n+1] = as[n];
as[n] = t;
}
n++;
}
n=0;
m--;
}
return as;
21
Árvore de Falhas para o
BubbleSort
Array desordenado
OR
While externo
não executado
While externo
executado m vezes
1. m  0 na primeira iteração
2. 0 as.length  1
3. Se as.length = 0, não há elementos
para ordenar
4. Se as.length = 1, o array está ordenado
5. Contradição
(...)
22
Árvore de Falhas para o
BubbleSort (2)
(...)
AND
0<m antes o
while externo
Um sub-conjunto das
iterações não ordena o array
corretamente
(...)
23
Árvore de Falhas para o
BubbleSort (3)
(...)
OR
While interno
não executado
1. m  n, na primeira iteração
While interno
executado m-1 vezes
para cada valor de m
2. n = 0, na primeira iteração
3. 0 < m
4. Por 2 e 3, n < m, na primeira iteração
(...)
5. Por 1 e 4, Contradição
(se o laço mais externo é executado pelo
menos uma vez, o mais interno também é)
24
Árvore de Falhas para o
BubbleSort (4)
(...)
AND
n<m antes o
while interno
Um sub-conjunto das
iterações não coloca o maior
elemento de as[0..m] na
posição m
(...)
25
Árvore de Falhas para o
BubbleSort (5)
(...)
OR
(...)
Primeira iteração:
(n-1)-ésima iteração:
n = 0 ^ v[0] > v[1]
=> swap(v[0], v[1])
n > 0 ^ v[n] > v[m]
=> swap(v[n], v[m])
Indutivamente, percebe-se que a
situação
Um sub-conjunto das
iterações não (...)
não ocorre
Primeira iteração:
n > 0 ^ v[n] < v[m]
=> skip
26
Características da Técnica

Vantagens:




Pode ser usada tanto para analisar confiabilidade
quanto segurança contra acidentes
Mais fácil de aplicar e entender do que uma
técnica inteiramente formal
Representação gráfica
Desvantagens:



Não garante a corretude da especificação
Pouco empregada, no contexto de software
Não provamos que o programa atende à
especificação
27
Roteiro




Introdução e Objetivos
Técnica 1: Cálculo de Refinamentos
Técnica 2: Árvore de Falhas
Conclusões
28
Conclusões




Técnicas que analisar e garantir
confiabilidade e segurança contra acidentes
são importantes, mas caras
Suporte de ferramentas pode amenizar esse
custo
Técnicas formais são extremamente
trabalhosas
Árvores de falhas são mais práticas, mas
fornecem menos garantias
29
Referências






T. Anderson e P. A. Lee. Fault Tolerance: Principles and Practice.
Prentice-Hall, 2a edição, 1990.
S. Coutinho, T. Reis e A. L. Cavalcanti. Uma ferramenta educacional de
refinamentos. Anais do XIII Simpósio Brasileiro de Engenharia de
Software - Sessão de Ferramentas, páginas 61-64, 1999.
N. Leveson. Software Safety: Why, What and How. ACM Computing
Surveys, 18(2):125-164, junho 1986.
C. Morgan. Programming from Specifications. Prentice-Hall, 2a edição,
1998.
J. D. Reese e N. Leveson. Software Deviation Analysis: A “Safeware”
Technique. 1996
Safeware Engineering Corporation. Verification of Safety. Disponível
para download em http://www.safeware-eng.com.
30