Applied Formal Methods

COM S 507

Offered during the Spring semester.

  1. Credits and contact hours: 3 credits
  2. Instructor’s or course coordinator’s name: Kristin Yvonne Rozier
  3. Text book, title, author, and year: No required textbook
  4. Other supplemental materialsPractical Formal Methods Using Temporal Logic, Michael Fisher, 2011

Specific course information

  1. Brief description of the content of the course: Introduction to formal methods; techniques for formal specification, validation, and verification of safety-critical systems; tools, techniques and applications of formal methods; emphasis on real-world use cases such as enabling autonomous operation.
  2. Prerequisites or co-requisites: AER E 361, or Com S 311 (required for Com S students), or an equivalent course and instructor permission
  3. Required, elective, or selected elective? Selected Elective

Specific goals for the course

  1. Specific outcomes of instruction: By the end of the course students should have a working knowledge and ability to learn  the following:
  • Specify system requirements formally in Linear Temporal Logic (LTL).
  • Specify systems as formal models.
  • Apply model checking to system models and  LTL  specifications to determine if the models satisfy the specifications.
  • Use tools popular in industrial verification labs, including explicit and symbolic model checkers, and theorem provers.
  • Evaluate real-world systems to determine appropriate formal methods to use in their analysis. (6)
  • Evaluate system requirements, including determining if they are safety or liveness, and performing basic specification debugging.
  • Analyze and draw conclusions about real-world systems regarding formal properties.
  • Explain the principles underlying formal methods for different types of system analysis (e.g. design time versus runtime), the capabilities, and the limitations.
  • Develop an understanding of the current state of the art and how to find formal methods tools for real-world use cases. (6)

Brief list of topics to be covered

  • Review of classical and propositional logic
  • Background on LTL: well-formed formulas, semantics, encoding English sentences, expressivity, normal forms, relationship to automata
  • Reactive system properties: reachability, safety, liveness, deadlock-freeness, fairness
  • Review of explicit and symbolic model checking
  • Specification and modeling of real systems
  • Deciding the truth of a temporal formula; related proof techniques including explicit model checking
  • Extensions including synthesizing software from specifications
  • Ideas for related formal methods, including timed automata models