Applied Formal Methods

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 materials: Practical 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