1
Validação Formal de Sistemas de
Software
Prof. Edward Hermann Haeusler
Depto de Informática PUC-RIO
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
2
Engenharia
- Aplicação da Ciência e Matemática através da qual as
propriedades da matéria e as fontes de energia são tornadas
úteis às pessoas (Dic. Merriam-Webster, 2001)
- Engenharia é a prática da aplicação segura e econômica das leis científicas que
governam as forças e materiais da Natureza, através da organização, design e
construção, para o benefício da humanidade.
S. E. Lindsay (1920)
- Desenvolvimento e Aplicação Sistemática de Modelos de Comprovada
Eficácia gerando Soluções Tecnológicas para Problemas da Humanidade
- Engineering is the application of math and science to create something of
value from our natural resources. (IEEE- 2002)
===> Projeto e Manufatura de Sistemas Complexos
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
3
Construção de um artefato para uso pela Sociedade
Levantamento
das
Características
Desejadas
Matemática e
Teorias Científicas
FABRICAÇÃO
Artefato
Validação
==> Métodos e Processos de Fabricação de Artefatos
- É mais econômico validar um processo de fabricação de um
artefato que um artefato individualmente.
==> Engenharia !!!
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
4
Construindo uma Ponte
Espec.
-Projeto
(template)
Cálculos
p/
Ponte
Implementação
-Fluxo
da Obra
-Recursos
humanos
-Material
-Profund.
-Ventos
-Correnteza.
- $$$
Física
Química
-Projeto
Físico
Matemática
Engenharia
- Carga
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
5
Engenharia de Software X Engenharias tradicionais
Aspecto
Eng. Software
Eng. Tradic.
Evolução do
artefato
Forma de
produção
Garantia do
Fabricante
Elic. de requis.
Adaptabilidade
Extremamente
dinâmica
Cópia do
executável
Lenta e
Gradual
Fabricação
das unid.
???????
Alguma
Complexa
Flexível
Simples
Rígido
==> As engenharias tradicionais baseiam-se fortemente em
“Frameworks” para construção de tipos bem específicos e
determinados de artefatos (aviões, carros, pontes, edifícios,
navios, etc).
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
6
Casos famosos de softwares complexos que não funcionaram a contento
- Explosão do foguete Ariadne (projeto europeu) poucos segundos após seu lançamento
devido a falha de programação.
- Sistema de triagem/controle de bagagem do aeroporto internacional de Denver (EUA)
atrasou a inauguração do aeroporto. Custo do sistema (193 milhões $$ ) :
- Inauguração estava prevista para Out/1993.
- Em Junho/1994 o sistema ainda não estava funcionando, mas custava $$ !!
- No começo de 1995 um controle MANUAL de bagagem foi instalado para
que o aeroporto pudesse ser inaugurado (com atraso de mais de um ano)
- O Therac-25, um equipamento de radioterapia controlado por computador, aplicou doses
fatais de radiação em alguns pacientes de câncer.
- Quando decidiram testar o subsistema de desligamento de emergência da Sizewell-B, uma
usina nuclear na Inglaterra, este falhou em mais de 50% das vezes. Não conseguiram encontrar a razão da falha nas 100.000 linhas de código.
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
7
O Conhecimento básico em Engenharia de Software compreende :
==> Lógica Matemática:
Trata das leis da argumentação (provas) formal.
==> Álgebra
Descreve leis de construção de “objetos” e determina a identidade entres estes.
==> Complexidade de Algoritmos e Computabilidade
Escopo e Limitações da noção de “computável”.
==> Experiência prévia com modelos de desenvolvimento de Software.
Apresenta métodos e técnicas de desenvolvimento em base empírica.
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
8
Métodos Formais e Arquitetura de Software
Porque Arquitetura de Software é essencial
para a validação de sistemas ??
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
9
Validação Formal e Arquitetura de Software
- Validação Formal de Software
x
Testes
- Sistemas Reativos e Transformacionais
- Como o projeto se reflete na etapa de validação
- Arquitetura de Software
- Adicionalmente o tempo aos requisitos funcionais
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
10
Verificação Formal
Testes
- Um passo de verificação pode
cobrir todo possível comportamento do sistema
Requisitos
Verificação
- Verificação antes da implementação diminui o custo $$ !!
Especificação
Testes
Implementação
TECMF
- É especialmente importante
quando o comportamento é
complexo.
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
11
Validação
x
Prova de Correção
Mundo
Real
cenários
Espec. Formal A
resultado
Espec. Formal
Verifica a adequação da
Especificação Formal
a Situações Reais
TECMF
Espec. Formal B
Prova que B tem as propriedades
que A também tem.
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
12
Métodos Formais
- Métodos Formais apresentam “frameworks” mentais, notações, e,
métodos sistemáticos para o projeto, documentação, e análise de
sistemas computação.
- Os principais benefícios da aplicação de métodos formais é permitir
que algumas questões sobre o projeto possam ser respondidas por
avaliação simbólica(e.g. prova de teorema ou verificação de modelo)
- A avaliação simbólica pode ser usada para “debugging” e inspeção do
projeto, bem como para verificação a posteriori.
- Pode ser comparado à forma com que cálculo estrutural é usado no
projeto de construções, mecânica computacional de fluídos é usada no
projeto de aeronaves, etc
- Bons para certificação e garantia de qualidade.
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
13
Técnicas Formais para a Validação de Sistemas
- Model Cheking (verificação de modelos)
Verificar se certas propriedades valem em um certo modelo
- Theorem Proving (prova de teoremas)
Provar propriedades em uma teoria sobre o sistema
Podem ser usados como métodos complementares
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
14
Model Checking: O que é ?
- Especificar
- O sistema como um sistema de transição (finito em geral).
- Uma propriedade como uma sentença em uma linguagem
de consulta.
- Estabelecer que o sistema é um modelo da sentença
sistema |= sentença
Obs: Tarefa realizada por varredura no espaço de busca
- Usualmente não há necessidade de teorias auxiliares
- Normalmente, as únicas suposições dizem respeito às propriedad
dinâmicas do sistema (branching vs. linear time, fairness, liveness
- Funciona melhor com sistemas voltados ao controle e com um
pequeno espaço de estados
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
15
Sistema
Reativo
Sistema
Transformacional
entradas
saídas
tempo
tempo
entradase saídas
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
16
- Sistemas Reativos podem ser entendidos como um conjunto de thre
concorrentes recebendo sinais de sensores no ambiente, e, atuand
sobre mecanismos que produzem a mudança desejada no ambiente
- Sistemas embutidos (dvd, injetor de combustível, celular) são
normalmente reativos
sensores
condic. da
entrada
interface
entrada
Processador
atuadores
TECMF
condic.
saída
interface
saída
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
17
Propriedades que são verificadas em S. Reativos (CMP1995)
Segurança (Safety) : “algo ruim nunca acontece”
 se uma resposta é dada então a mesma está correta
 Toda vez que a porta do avião abre, há uma escada.
 Não há ``deadlocks''
Progresso (Liveness) : “algo bom acontece”
Garantia : “algo pode acontecer”. Ex: O vídeo pode ser repetido
Obrigação : “algo sempre acontece”. Ex: O motor sempre funciona.
Atividade : “sempre a postos”. Ex: Toda requisição é atendida.
Persistência : Uma vez a porta fechada, sempre é possível abrí-la
Reatividade = Atividade & Persistência
Oportunidade (Fairness) :
“se algo pode acontecer então ocorre infinitas vezes”
“se algo pode acontecer infinitas vezes então acontece infinitas vezes
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
18
Especificação (modelo) de sistemas reativo
Threads/Processos + Composição
- Abordagens :
- Algébra + Lógica (CCS/Pi-calculus + -calculus)
- Modelo + Lógica (Mundos Possíveis + Lógica Temporal)
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
Mundos Possíveis (Kripke)
- A verdade de uma proposição é verificada em relação à um
mundo.
- Os mundos estão relacionados ao tempo (lógica temporal)
- Mundos podem ser vistos como estados locais/globais.
- Estrutura ramificada, ou, linear de tempo. (obs: ¬ P  P )
•P
•P
P,Q ,•P
P,Q ,•P
P,•Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q ,•P
P,Q
P,Q
•P  Sempre P  AP
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
19
20
Outras modalidades temporais
PUQ
EP
NP
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,•P
P,Q ,EP
P,Q ,•P
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q
P,Q
PUQ  P until Q
NP  Next P
EP  Eventualmente P  P
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
21
O Until e o Next são suficientes
TECMF
-
true U P  EP
-
AP  ¬ E ¬ P
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
22
Threads e Máquinas de Estado Finitas
- Cada Thread pode ser modelada por uma MEF
act2
3
act2
2c
2c
Est.
1
cond/act1
Est.
2
ev2
ev2
ev1
act2
act2
ev2
3
1
act2
2c
act1
3
act1
2c
act2
ev1
ev2
ev2
3
1
3
ev1
3
3
act2
ev2
3
3
ev2
3
act2
2c
act1
2c
1
ev2
3
ev1
act2
2c
act1
1
2c
3
ev2
3
ev1
3
MEF
Comportamento da MEF
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
23
Alarme de Cofre
sound
alarm
count = = 3
/count = 0
enter
code code entered
check
code
TECMF
invalid code/
count ++
valid code/count = 0
timeout
delay
count
attempts
unlock
door
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
24
Model Checking
- Usualmente se usa estrutura de tempo ramificado (branching time)
e CTL como linguagem lógica de consulta
(CTL = Computational Tree Logic)
- CTL : CTL apresenta quantificação sobre caminhos e sobre estados
-
AG(p) : p é verdade em todo estado ao longo de cada caminho.
AF(p) : p é verdade em algum estado ao longo de cada caminh
EG(p) : p é verdade em todo estado ao longo de algum caminho
EF(p) : p é verdade em algum estado ao longo de algum caminh
Inclui “next” e “until” e invariantes “fair”
(O modelo só é verificado para os caminhos onde a condição de
Fairness vale em uma quantidade infinita de estados)
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
25
Threads and Finite State Machines
- Each thread can be modeled by a finite state machine
count = = 3
sound /count = 0
count
alarm
attempts
enter
code code entered
check
code
valid code/count = 0
timeout
delay
TECMF
invalid code/
count ++
unlock
door
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
26
- Checking
AG(enter_code & valid_code ===> AF(unlock_door))
results in “true”
- Checking
AG(enter_code ===> AF(unlock_door))
results in the following computation path as a counter-example
enter
code
check
code
count
attempts
sound
alarm
3 times
enter
code
check
code
count
attempts
3 times
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
27
The whole system as an async. product of state machines
3
11
21
2
1
X
1
22
=
12
23
13
2
State Explosion !!!!!!
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
28
Semáforo
fora da
região crítica
fora da
região crítica
1
entrando
entrando
saindo
entrando
!semaforo
na região
crítica
TECMF
!semaforo
0
na região
crítica
saindo
saindo
processo1
processo2
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
29
Problema
- Considere uma pizzaria com 3 fornos. Por razões de segurança,
somente dois fornos podem ser abertos por vez. Mesmo assim,
toda vez que dois fornos são abertos, para evitar sobrecarga, o
terceiro forno deve estar em pré-aquecimento.
- Uma pizza leva 30 min para estar pronta, após 5 minutos de
pré-aquecimento, e, se o tempo passar de 30 min a pizza ficará
queimada.
=> Projetar o sistema de controle de abertura de portas de forno e
gerenciamento da fabricação de pizzas
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
30
xaberto&
yaberto
sem_vai_abrir
fechado
vai_assar
!passou5 v
passou5 &
(passou5 & !sem_vai_assar
!sem_vai_assar)
aberto
pre_aquec
!passou30
assando
passou30 &
sem_vai_abrir
!xaberto&
yaberto
!sem_vai_abrir
xaberto&yaberto
!(xaberto&
yaberto)
vai_abrir
passou30 &
!sem_vai_abrir
!(aberto(1)&aberto(2)&aberto(3)) // só 2 fornos abertos por vez
!(assando&passou30) // não pode queimar pizza
!(aberto(1)&aberto(2)&assando(3)) // não pode
!(aberto(1)&assando(2)&aberto(3)) // ter
Estado
Região
Crítica
!(assando(1)&aberto(2)&aberto(3)) // sobrecarga
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
31
Em SMV
MODULE main
VAR
sem_vai_assar : boolean ;
sem_vai_abrir : boolean ;
forno1 : process forno(sem_vai_assar,sem_vai_abrir,forno2.state,forno3.state) ;
forno2 : process forno(sem_vai_assar,sem_vai_abrir,forno1.state,forno3.state) ;
forno3 : process forno(sem_vai_assar,sem_vai_abrir,forno1.state,forno2.state) ;
ASSIGN
init(sem_vai_assar) := 0 ;
init(sem_vai_abrir) := 0 ;
SPEC
!EF(forno1.state = aberto & forno2.state = aberto & forno3.state = aberto) &
!EF(forno1.state = aberto & forno2.state = aberto & forno3.state = assando) &
!EF(forno1.state = aberto & forno2.state = assando & forno3.state = aberto) &
!EF(forno1.state = assando & forno2.state = aberto & forno3.state = aberto) &
!EF(forno1.state = assando & forno1.passou30 = 1 & forno1.running=1 & EX(forno1.state = assando)) &
!EF(forno2.state = assando & forno2.passou30 = 1 & forno2.running=1 & EX(forno2.state = assando)) &
!EF(forno3.state = assando & forno3.passou30 = 1 & forno3.running=1 & EX(forno3.state = assando))
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
32
MODULE forno(sem_vai_assar,sem_vai_abrir,xstate,ystate)
VAR
state : { fechado, aberto, pre_aquec, assando, vai_abrir, vai_assar } ;
passou5 : boolean;
passou30 : boolean;
ASSIGN
init(state) := fechado ;
next(state) :=
case
state = fechado & ! sem_vai_abrir : vai_abrir;
state = aberto : { aberto, pre_aquec } ;
state = pre_aquec & passou5 & ! sem_vai_assar : vai_assar ;
state = assando & passou30 & ! sem_vai_abrir : vai_abrir ;
state = assando & passou30 : fechado ;
state = vai_assar & (xstate = aberto) & (ystate = aberto) : pre_aquec ;
state = vai_assar : assando ;
state = vai_abrir & ((xstate = aberto) & (ystate = aberto) | ((xstate = aberto & ystate = assando) | (ystate = aberto & xstate = assando))): fechado ;
state = vai_abrir : aberto ;
1 : state ;
esac ;
next(sem_vai_assar) :=
case
state = vai_assar : 1 ;
state = pre_aquec | assando : 0 ;
1 : sem_vai_assar ;
esac ;
next(sem_vai_abrir) :=
case
state = vai_abrir : 1 ;
state = fechado | aberto : 0 ;
1 : sem_vai_abrir ;
esac ;
next(passou30) :=
case
1: { 0, 1 } ;
esac ;
next(passou5) :=
case
1: { 0, 1 } ;
esac ;
FAIRNESS
running
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
33
Types of Real-Time embedded systems
Hard - where not meeting a deadline is a failure
Soft - where deadline can be missed and the system may still
work if it is possible to recover
Slow - the system will have to respond within seconds
Fast - the system has to respond within a second
(typically within mili- or microseconds
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
34
Characteristics of RT-Reactive Systems
response time deadline The system must respond to the environment within a specified
time after the input has been recognized
validity of the data The inputs may become obsolete with time. The interval for
which input data is valid must be take into account for proc.
requirements.
periodic execution Reactive systems tend to collect data at predetermined time
intervals.
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
35
Timed Automata as a model for RT-Reactiveness
- Clock-variables and time/delay conditions for
enabling transitions
- Can be enriched with other data-type variables (global vars)
- Communication by means of channels (CSP-style)
Est.
1
C >= 2,4
req?
Est.
2
req!
v[i]:= C
reset
start
T <= r
C := 0
i++
3
i := 0
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
36
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
37
Theorem Proving:
O que é ?
- Especificar
- O sistema (em algum nível adequado de abstração)
- Propriedades requeridas do sistema.
- Suposições (restrições de ambiente, usuário, etc)
- Teorias sobre os tipos de dados envolvidos
- E provar que:
Teorias+Suposições+Sistema |-- requisitos
- Variação:
- Provar que a implementação é um refinamento da especificação
- Funciona melhor em sistemas com intenso tratamento de dados
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
38
Teoria sobre os Números Naturais
"x(s(x)  0)
"x"y( s(x) = s(y) x = y)
"y(y  0 x( s(x) = y) )
(P(0) & "x(P(x) P(s(x)))) "xP(x)
Especificação Lógica de um Tipo de dado
Teoria |-- Prop
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
39
Semântica Axiomática de uma LP
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
40
Prova de correção de código
Teoria
Teoria
Teoria
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
41
Software Architecture = components + structure
Architectural connectors
- Sequential Composition
- Parallel synchronous composition
- Parallel asynchronous composition *
- Behavior inheritance
- Factorization of common Behaviors
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
42
An Example: Harel Statecharts
- Conditions and Actions
?condition
!action
- Design Hierarchy
- On-entry, on-exit during actions
- Independent Threads of Control
- Visual synchronization/complex Transition (as in Petri-nets)
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
43
Pattern used in ARTS
(Haeusler & Fontoura 99)
- Horizontal Composition
Car
sync(b_off,link)
sync(b_on,unlink)
Motor
Brake
t_off
Off
b_off
M
b_on
On
t_on
S
link
unlink
L
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
44
In categorial terms the horizontal composition is a Colimit
CatL
x={,}
Th(x)
b_on
b_off
Th(Brake)
link
unlink
Th(Motor)
Th(Car)
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
45
Mathematicaly
OO Projects
TTS
RETOOL
Theories
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
46
Gen. of
RETOOL
Theories
OO
Projects
Projects
Base
RETOOL
Theorem
Prover
CORBA
Model-Chec.
Spec.
Generation.
Gen. of
C++
Code
TECMF
Formal
Validation
Layer
ModelChecker
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
47
Projeto MEFIA - CNPq/NSF
Mathematical and Engineering Foundations for
Interoperability via Architecture
- Formally based Software Architectures
- Tools and Techniques for the Software Development Process
- Compositionality
partners: PUC-Rio, UFRGS, Stanford Univ, SRI, Univ. of Illinois
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
48
- Cada Model-Checker trata com técnicas e abordagens
diferentes o problema de especificações com grande
número de estados
SMV - BDD’s
SPIN - Supertrace
UppAll - Prog. Lógica
Hytech - Diferenças finitas + varredura simples
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
49
Alguns “detalhes” importantes :
1- A menos que P=NP não existe um sistema de prova
eficiente (polinomial) para a lógica proposicional.
2- A lógica de primeira ordem é indecidível.
3- Composicionalidade é uma propriedade que não coexiste
muito bem com concorrência.
==> Lógicas modais (doxástica, deôntica, epistêmica e suas versões
multi-agentes (multi-modais) também têm modelos de Kripke como
semântica).
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.
50
Métodos e Modelos importantes :
CCS - Álgebra de processos com teoria de equivalência e
lógica associada (-calculus).
Pi-Calculus - Álgebra de processos que inclui abstração sobre
canal de comunicação e conseguente habilidade
de especificar mobilidade.
Redes de Petri - Modelo não composicional de concorrência real
(true concurrency)
Autômatos Híbridos - Levam a variação em conta (derivada em
relação ao tempo)
Model-checkers - CWB, MWB e simulação em redes de petri
TECMF
Prof. E.H.Haeusler
Métodos Formais no
Desenvolvimento de Sist.