Exploring the constraints in formal verification of communication and computing systems

The high cost of correcting errors in digital design and communication protocols of e-economy systems calls for creative formal verification methods. Unlike testing and simulation, formal verification methods cover the entire system state space and all possible combination of inputs. There are two common approaches to the problem of formal verification: theorem proving and model checking. Since the deductive approach in theorem proving has many noted shortcomings the focus of the paper is on the model checking techniques. The paper explores the constraints of the application of the verification process, finds the most difficult steps in terms of space and time complexity and proposes the necessary operations to strengthen the methodology and expand it to real-world sized examples. The state explosion problem is tackled by applying binary decision diagrams (BDD) diagrams that can efficiently represent relations (functions) and sets. Finally, the paper suggests some general research directions that are likely to lead to technological advances.