Sérgio Vale Aguiar Campos

This page in English

Área de Pesquisa

  • Saiba o que é.
  • Veja na prática como funciona.
  • Ou então leia mais a respeito.
  • Outras referências

    • Verificação Automática de Sistemas Distribuídos e de Tempo Real

    Técnicas de verificação automática e suas aplicações a problemas práticos. Verificação e análise de sistemas distribuídos e de tempo real.

    A tarefa de se verificar se um sistema computacional satisfaz suas especificações é extremamente importante. Tais sistemas são usados frequentemente em aplicações aonde uma falha pode ter consequencias muito sérias, em alguns casos até fatais. Meu trabalho propõe um método eficiente para se efetuar esta verificação. O método é baseado em verificação de modelos usando lógica temporal (temporal logic model checking), uma técnica para verificação de sistemas reativos. No método proposto um sistema de tempo real é representado por um grafo finito que é implementado por diagramas de decisão binários (BDDs). Algoritmos simbólicos eficientes exploram o grafo para determinar se o sistema satisfaz ou não as especificações.
    Esta técnica foi usada na verificação de vários sistemas de complexidade industrial tais como controladores de aeronaves, sistemas de robótica e o PCI local bus, demonstrando que o método proposto pode ser usado para ajudar a resolver problemas práticos.

    Verus - Um Compilador/Verificador para Sistemas de Tempo Real

    Para saber um pouco mais sobre Verus consulte o (curto) artigo abaixo:

    S. Campos, E. Clarke and M. Minea. The Verus tool: a quantitative approach to the formal verification of real-time systems. In: Conference on Computer Aided Verification, 1997.
    Postscript

    Você pode instalar Verus e testemunhar na prática todas suas vantagens (e desvantagens):

  • Verus: verus0.9.tar.gz (92K)
  • BDD library: bddlib.tar.gz (100K)
    • Observações:
  • O código executa sem alterações no sistema linux, mas modificações para variações de unix são simples.
  • É necessário instalar o pacote de BDDs antes de instalar Verus.
  • Manuais, licensa de uso, exemplos e tudo mais é encontrado junto com o código.

    • Artigos

  • S. Campos and E. Clarke, The Verus language: representing time efficiently with BDDs. Fourth AMAST Workshop on Real-Time Systems, Concurrent, and Distributed Software, 1997.
    Abstract , Postscript

  • S. Campos, E. Clarke and M. Minea. Symbolic techniques for formally verifying industrial systems. In: Science of Computer Programming, special issue on Industrially Relevant Applications of Formal Analysis Techniques, 29, pp. 79-98, Elsevier Science, 1997.
    Abstract , Postscript

  • S. Campos, E. Clarke and M. Minea. The Verus tool: a quantitative approach to the formal verification of real-time systems. In: Conference on Computer Aided Verification, 1997.
    Postscript

  • S. V. Campos, E. M. Clarke, W. Marrero and M. Minea. Verifying the performance of the PCI local bus using symbolic techniques. In: International Conference on Computer Design, 1995.
    Abstract , Postscript

  • S. Campos, E. Clarke, W. Marrero and M. Minea, Verus: a tool for quantitative analysis of finite-state real-time systems. In: Workshop on Languages, Compilers and Tools for Real-Time Systems, 1995.
    Abstract , Postscript

  • S. Campos, E. Clarke, W. Marrero, M. Minea and H. Hiraishi, Computing quantitative characteristics of finite-state real-time systems. In IEEE Real-Time Systems Symposium, 1994.
    Abstract , Postscript
  • S. Campos. A Quantitative Approach to the Formal Verification of Real-Time Systems. Ph.D. Thesis, SCS, Carnegie Mellon University, 1996.
    Postscript

    • Para maiores informações uma boa fonte é:

    Carnegie Mellon's model checking project home page

    De volta a página principal