Symbolic Model Checking in Practice

Sérgio Vale Aguiar Campos

Symbolic model checking is a technique for verifying finite state reactive systems that has been very successful in practice. In this method a system being verified is represented by a state transition graph. Efficient search algorithms are used to determine if the model satisfies properties expressed as temporal logic formulas. The internal representation of the model checker uses binary decision diagrams - BDD, an extremely compact representation of boolean formulas. Because of the BDD representation it is possible to verify extremely large and complex systems, such as aircraft controllers, robotic controllers, the PCI local bus and the future bus+ protocols. This work presents the method and discusses how it can be applied in practice.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: