A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> From Simulation and Testing to Formal Verification <s> Part I. Tutorial: 1. Introduction to ML 2. The HOL logic 3. Introduction to proof with HOL 4. Goal-oriented proof: tactics and tacticals 5. Example: a simple parity checker 6. How to program a proof tool 7. Example: the binomial theorem Part II. The Meta-Language ML: 8. The history of ML 9. Introduction and examples 10. Syntax of ML 11. Semantics of ML 12. ML types 13. Primitive ML identifier bindings 14. General purpose and list processing functions 15. ML system functions Part III. The Hol Logic: 16. Syntax and semantics 17. Theories Part IV. The Hol System: 18. The HOL logic in ML Part V. Theorem-Proving With HOL: 19. Derived inference rules 20. Conversions 21. Goal-directed proof: tactics and tacticals Appendices. <s> BIB001 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> From Simulation and Testing to Formal Verification <s> Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, and request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature. <s> BIB002
The definition of correctness of routing protocols may consist of several aspects, such as stability, loop-freedom etc. The various key properties may be verified with different techniques, of which the two most important techniques are: traditional simulation and testing, and more recent formal verification. Simulation and testing  are the most practiced techniques for verifying the correctness of routing protocols, since they are well understood by engineers and easy to use. The simulations of protocols can be automatically tested using computers (e.g. ns2), and the implementations of protocols can be tested on a real ad hoc network. Some faults can be discovered during simulation and testing, and then fixed by engineers. Thus, they can improve the probability that a protocol achieves the desired functions. However, the most important shortcoming of simulation and testing is coverage. Note that we would first have to fix the network size and topology, then run the protocol for a limited length of time. A testing procedure starts from a given initial state, and only a single execution is observed and checked. Although the result is informative, it does not provide a complete verification, since a full proof should guarantee the correctness on all networks, over all lengths of time, under all possible initial states, and for every sequence of events that can occur. Since simulation and testing cannot cover all these cases in running a protocol (and the coverage cannot be proved even if it is actually sufficient), they reduce the level of assurance in correctness. Indeed, there may be some subtle faults that remain hidden in a few tests, but might lead to serious failures in future operations. Formal verification (or formal method) is a kind of mathematical reasoning about systems. Formal verification provides more trustable verification results, thanks to their exhaustive searching of all possible executions. This means, if it is proved that a protocol satisfies some properties, then the result holds for all cases on all networks. The invention of some automated analysis techniques makes formal verification more and more feasible in practice. For instance, model checkers [12, BIB002 can automatically enumerate all possible executions of a system, and verify a property over these executions, while theorem provers BIB001 provide automated formal support for the creation and checking of proofs. However, model checkers suffer the state explosion problem 1 , and the weakness of theorem provers is the significant user intervention. We believe that, the combination of manual mathematical reasoning, automated model checking and automated theorem proving is a more practical alternative for verifying large(-scale) systems.