Model Checkers: Uma análise de ferramentas para a linguagem de programação C TRABALHO DE GRADUAÇÃO

Model Checkers: Uma análise deferramentas para a linguagem de

programação C

TRABALHO DE GRADUAÇÃOTRABALHO DE GRADUAÇÃO

Pedro Montenegro Pedro Montenegro

([email protected])([email protected])

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



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


Abordagens da técnicaAbordagens da técnica

Bounded Model Checking (BMC)Bounded Model Checking (BMC)

Abstração de predicadosAbstração de predicadosUsando um provador de teoremasUsando um provador de teoremas

Usando resolvente SATUsando resolvente SAT

Migração de C para outro modeloMigração de C para outro modelo


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


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


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 programa

Verificador 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



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


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


A versão atual não suporta ponteiros para função

Funções recursivas não são suportadas


MOPSMOPS


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


Precisão afetada por priorizar a escalabilidade e ignorar o

fluxo de dados


CBMCCBMC


A principal é o suporte a maioria das estruturas de C

– Escalabilidade é um grande diferencial do CBMC

Usa um resolventes SAT

Interface amigável


Não poder provar a ausência de erros na maioria dos casos

reais

Por priorizar a escalabilidade, a precisão é comprometida



Três propriedades são consideradas:

Soundness

Completeness

Termination


Difícil apontar uma ferramenta que seja a melhor

Para cada situação uma ferramenta pode se encaixar melhorDepende das características do código C do programa que se quer

analisar

Da forma mais geral possível

BLAST

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

componente

Problemas como comportamento indesejado

Determinar a alcançabilidade dos estados implementados no

componente

Utilização de um plugin para o eclipse


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)



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



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

Documents

Model Checkers: Uma análise de ferramentas para a linguagem de programação C TRABALHO DE GRADUAÇÃO