COM S 407
Offered during the Spring semester.
- Credits and contact hours: 3 credits
- Instructor’s or course coordinator’s name: Kristin Yvonne Rozier
- Text book, title, author, and year: No required textbook
- Other supplemental materials: Practical Formal Methods Using Temporal Logic, Michael Fisher, 2011
Specific course information
- 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.
- Prerequisites or co-requisites: AER E 361, or Com S 311 (required for Com S students), or an equivalent course and instructor permission
- Required, elective, or selected elective? Selected Elective
Specific goals for the course
- 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