View
219
Download
1
Category
Preview:
Citation preview
Model Checkers: Uma análise deferramentas para a linguagem de
programação C
TRABALHO DE GRADUAÇÃOTRABALHO DE GRADUAÇÃO
Pedro Montenegro Pedro Montenegro
(pmr@cin.ufpe.br)(pmr@cin.ufpe.br)
2007.12007.1
ContextoContexto IntroduçãoIntrodução ObjetivosObjetivos Model CheckingModel Checking Ferramentas para a linguagem CFerramentas para a linguagem C Análise das FerramentasAnálise das Ferramentas Estudo de CasoEstudo de Caso ConclusãoConclusão Trabalhos FuturosTrabalhos Futuros
ROTEIROROTEIRO
Cooperação de pesquisa entre o CIn/UFPE e uma Cooperação de pesquisa entre o CIn/UFPE e uma Empresa de São PauloEmpresa de São Paulo
Sistema do complexo de metrô de Santiago no Sistema do complexo de metrô de Santiago no
ChileChile Componente crítico do metrôComponente crítico do metrô
Controladora Geral de Portas (CGP)Controladora Geral de Portas (CGP) Casos de UsoCasos de Uso
Função abre portasFunção abre portas
Função fecha portasFunção fecha portas
ContextoContexto
Sistemas críticos necessitam de garantia de Sistemas críticos necessitam de garantia de funcionamento perfeitofuncionamento perfeito
Falhas podem levar a perdas financeiras ou de Falhas podem levar a perdas financeiras ou de vidas humanasvidas humanas
Um dos pontos fundamentais para garantir esse Um dos pontos fundamentais para garantir esse
alto nível de qualidade é a análise formal de alto nível de qualidade é a análise formal de
propriedadespropriedades
Necessidade de suporte ferramental que Necessidade de suporte ferramental que
automatize o processo de verificaçãoautomatize o processo de verificação
IntroduçãoIntrodução
Procurar Ferramentas Model Checkers para Procurar Ferramentas Model Checkers para a linguagem de Programação Ca linguagem de Programação C
Análise das ferramentas mais utilizadas em Análise das ferramentas mais utilizadas em relação as características, as abordagens relação as características, as abordagens que utilizam, as vantagens e desvantagens que utilizam, as vantagens e desvantagens
Apontar a ferramenta que apresentou os Apontar a ferramenta que apresentou os melhores resultados para o contexto do melhores resultados para o contexto do trabalhotrabalho
ObjetivosObjetivos
Nos últimos anos as indústrias reconheceram os Nos últimos anos as indústrias reconheceram os verificadores de modelos como uma ferramenta verificadores de modelos como uma ferramenta promissora para o desenvolvimento de sistemaspromissora para o desenvolvimento de sistemas
Provou ser uma tecnologia bem sucedida para Provou ser uma tecnologia bem sucedida para verificar exigênciasverificar exigências
Técnica totalmente automática que analisa o espaço Técnica totalmente automática que analisa o espaço de estados finito de sistemas críticosde estados finito de sistemas críticos
Verifica automaticamente a validade de propriedades Verifica automaticamente a validade de propriedades acerca do comportamento de sistemasacerca do comportamento de sistemas
Model CheckingModel Checking
Model CheckingModel Checking
Para realizar a validação das propriedades de Para realizar a validação das propriedades de
sistemas seguem-se três passos:sistemas seguem-se três passos:
ModelagemModelagem
EspecificaçãoEspecificação
VerificaçãoVerificação
Tipos de PropriedadesTipos de Propriedades SegurançaSegurança Atingibilidade (Reachability)Atingibilidade (Reachability) Razoabilidade (Fairness)Razoabilidade (Fairness) Ausência de DeadlockAusência de Deadlock Vivacidade (Liveness)Vivacidade (Liveness)
Verificação de Modelos na práticaVerificação de Modelos na prática Problemas como a explosão de estados e Problemas como a explosão de estados e
especificação de propriedadesespecificação de propriedades Estratégias Estratégias
Model CheckingModel Checking
Abordagens da técnicaAbordagens da técnicaBounded Model Checking (BMC)Bounded Model Checking (BMC)Abstração de predicadosAbstração de predicados
Usando um provador de teoremasUsando um provador de teoremasUsando resolvente SATUsando resolvente SAT
Migração de C para outro modeloMigração de C para outro modelo
Model CheckingModel Checking
SLAMSLAM Impulsionou o uso de verificação de modelosImpulsionou o uso de verificação de modelos Usado com sucesso em Device Drivers do Windows
O SLAM tem três componentes principais:
c2bp - avalia um abstração booleana do programa
bebop - executa a análise da atingibilidade de
programas booleanos
newton - verifica a praticidade dos caminhos de erros
O SLAM usa o zapato como seu provador de teorema
FerramentasFerramentas
FerramentasFerramentas
BLASTBLAST A abordagem é a mesma seguida no SLAM
Usa conceitos de abstração “preguiçosa”
Composto pelo spec.opt e pblast.opt
Usa “Simplify” e “vampyre” como provadores de
teorema
FerramentasFerramentas
MOPSMOPS Ferramenta de análise estática Abordagem baseada em CFG (gráfico do fluxo de controle) Consiste em um “parser” e um verificador de modelos
Parser - constrói um CFG do programaVerificador de modelos - constrói um PDA do CFG e verifica
se o PDA vai de encontro à propriedade de segurança
CBMCCBMC Bounded Model Checker (verificador de modelos limitado)
Usa um resolvente SAT
Procura por um contra-exemplo, limitado por algum inteiro
N.
Na maioria dos casos CBMC pode determinar o limite
superior N. Se falhar, o usuário pode então fornecer um
limite superior
Usada como ferramenta para encontrar erros e não
provar a exatidão
FerramentasFerramentas
FerramentasFerramentas
SATABSSATABS MAGIC / ComFoRTMAGIC / ComFoRT Resumo das ferramentasResumo das ferramentas
SLAMSLAM PotencialidadesPotencialidades
Sucesso com Device DriversSucesso com Device Drivers
Suporta procedimentos recursivos Limitações Limitações
Tratamento dos ponteiros
– Abstrair de uma linguagem com ponteiros (C) a uma
sem ponteiros (programas booleanos) é difícil
Foco no domínio da aplicação de Device Drivers
Parte de um produto comercial (SDV) da Microsoft
Atualmente, não suporta programas muito grandes
Análise de FerramentasAnálise de Ferramentas
BLASTBLAST PotencialidadesPotencialidades
Usa a abstração sob demanda para reduzir o refinamento
desnecessário da abstração
– Economiza espaço e tempo
Atualmente, diz suportar muitas construções sintáticas de C,
incluindo estruturas e procedimentos
Encontrou erros em diversos Drivers
Limitações Limitações
A versão atual não suporta ponteiros para função
Funções recursivas não são suportadas
Análise de FerramentasAnálise de Ferramentas
MOPSMOPS PotencialidadesPotencialidades
Escalabilidade e eficiência por considerar somente o fluxo
de controle e por ignorar a maioria do fluxo de dados
Habilidade em relatar somente um “trace” de erro para cada
causa do erro
– Reduz significativamente o número de erros que o
programador tem que rever
Limitações Limitações
Precisão afetada por priorizar a escalabilidade e ignorar o
fluxo de dados
Análise de FerramentasAnálise de Ferramentas
CBMCCBMC PotencialidadesPotencialidades
A principal é o suporte a maioria das estruturas de C
– Escalabilidade é um grande diferencial do CBMC
Usa um resolventes SAT
Interface amigável Limitações Limitações
Não poder provar a ausência de erros na maioria dos casos
reais
Por priorizar a escalabilidade, a precisão é comprometida
Análise de FerramentasAnálise de Ferramentas
Análise de FerramentasAnálise de Ferramentas
Três propriedades são consideradas:SoundnessCompletenessTermination
Análise de FerramentasAnálise de Ferramentas
Difícil apontar uma ferramenta que seja a melhor Para cada situação uma ferramenta pode se encaixar melhor
Depende das características do código C do programa que se quer analisar
Da forma mais geral possívelBLAST
Análise das estruturas de C utilizadas no componenteAnálise das estruturas de C utilizadas no componente Ferramenta utilizada : CBMCFerramenta utilizada : CBMC
Utilização da função assert
Verificação do estado que se encontra o programa e suas
variáveis de controle depois da execução de uma função do
componenteProblemas como comportamento indesejado
Determinar a alcançabilidade dos estados implementados no
componente
Utilização de um plugin para o eclipse
Estudo de CasoEstudo de Caso
Variáveis do sistema precisaram ser declaradas no componente Os nomes das variáveis foram trocados
Uma função main foi declarada Velocidade máxima para abertura de portas
Documento de requisitos -> 6Km/h Código -> 3Km/h
Foram verificados diversos fluxos do sistema, sendo que dois deles foram selecionados e relatados: Um fluxo de uma operação de abrir e fechar portas com velocidade
menor que 3Km/h A verificação da alcançabilidade dos estados após a execução da
função n vezes através do comando “while” (n limitado pela ferramenta)
Estudo de CasoEstudo de Caso
Estudo de CasoEstudo de Caso
Exemplo do primeiro fluxo selecionado:
Com relação ao outro fluxo selecionado, um potencial problema foi
encontrado
Foi escolhido um valor limite para as iterações do loop ao qual a
função foi submetida
Valor que levasse em conta um grande número de análises e
não levasse muito tempo para fazer as verificações
Problema com relação a atingibilidade do estado 6
Apesar de haver a possibilidade da variável ser alterada em
outro componente do sistema
Análise foi feita somente em relação ao componente,
considerando apenas as atribuições feitas pela função
Estudo de CasoEstudo de Caso
Estudo de CasoEstudo de Caso
A estratégia adotada foi a colocação do
assert(CGP_informarProximoEstadoDireita_MEMORIA<=5). Mostrando que o assert é sempre verdade, mostro que a variável de
estado nunca assume valores maiores que 5, ou seja, não assume o
valor 6, e conseqüentemente, o estado 6 não foi alcançado.
Difícil apontar uma ferramenta que seja a melhor
Para cada situação uma ferramenta pode se encaixar melhor
Depende das características do código C do programa
Programas Seqüenciais
Extensões estão sendo desenvolvidas para programas
concorrentes.
Algumas estruturas de C ainda não são suportadas
Tanto as ferramentas quanto as abordagens ainda têm muito a
evoluir
Pesquisas estão sendo realizadas nesse sentido
ConclusãoConclusão
Procura de ferramentas Model Checkers para a linguagem
C.
Descrição e análise das abordagens utilizadas pelas
ferramentas para a linguagem C.
Descrição do funcionamento das principais ferramentas.
Análise das principais características das ferramentas mais
utilizadas.
Aplicação prática de um Model Checker em um componente
do metrô, relatando os resultados obtidos, as verificações
realizadas e os problemas encontrados.
ContribuiçõesContribuições
Estudo mais aprofundado da utilização da lógica temporal
nas ferramentas
Formulação de propriedades importantes na lógica
temporal que um sistema crítico precisa validar
Submeter estas propriedades às diversas ferramentas
e relatar os resultados
Estudo de possíveis melhorias das ferramentasEstudo de possíveis melhorias das ferramentas
Abordagem utilizadaAbordagem utilizada
ImplementaçãoImplementação
Trabalhos FuturosTrabalhos Futuros
Recommended