engleski

BDD-based Algorithms for Computing State Transitions

Symbolic model checking is used extensively to verify finite-state systems by examining state-graph models of the system behavior. The algorithmic nature of model checking procedure makes it fully automatic but at the same time sensitive to the size of the formal model of the system. The binary decision diagram (BDD) is a powerful data structure for the representation of many mathematical objects and specifically suitable for the valid state space computation. The aim of the paper is to identify the computationally expensive BDD operations with respect to the size of the state graph. Based on these operations the paper presents a study of performance issues and possible improvements in BDD construction and manipulation.

formal methods; BDD-based algorithms; formal verification

nije evidentirano