Become familiar w/ model checker & analyzer  Choose a specific domain of networking: Routing in mobile ad-hoc networks Formalize safety and correctness properties in later slides  Make use of formalizing tool, model checker SPIN Confirm counter-example  assertion with violation of each property is inserted