This textbook gives students a comprehensive introduction to formal methods and their application in software and hardware specification and verification. It has three parts: The first part introduces some fundamentals in formal methods, including set theory, functions, finite state machines, and regular expressions. The second part focuses on logic, a powerful formal language in specifying systems properties. It is composed of four chapters: propositional logic, predicate logic, temporal logic, and model checking. The third part presents the most popular formal language in system behavior modeling, Petri nets. It has three chapters: Petri nets, timed Petri nets and high-level Petri nets.
Part 1: Fundamentals; Chapter 1: Set Theory and Functions; Chapter 2: Finite-state Machine; Chapter 3: Regular Expression and Formal Languages; Part 2: Specify Software System Properties with Logic; Chapter 4: Propositional Logic; Chapter 5: Predicate Logic; Chapter 6: Temporal Logic; Chapter 7: Formal Verification; Part 3: Model System Behavior with Petri Nets; Chapter 8: Petri Nets; Chapter 9: Timed Petri Nets; Chapter 10: High-level Petri Nets.