Formal Methods in Computer Science

Students of software and hardware design can use this textbook to learn formal methods, the mathematical techniques used to specify and verify computing systems. The opening section covers foundations such as set theory, functions, finite state machines, and regular expressions, giving readers the groundwork for the material that follows.

The middle section is devoted to logic as a means of stating what a system must do. It moves through propositional logic, predicate logic, and temporal logic, then shows how model checking can be used to test those properties against a system.

The final section turns to Petri nets, a widely used notation for modeling how systems behave. Beyond standard Petri nets, it introduces timed Petri nets and high-level Petri nets. Throughout, the author emphasizes practical uses for each technique and includes a set of exercises to reinforce the concepts. Readers can also download source code for non-commercial use.

The book is written for undergraduate and graduate courses in computer engineering, software engineering, computer science, and information technology. Some chapters suit undergraduate computing courses, and the book also works as a reference for researchers working on formal specification and validation.