Academics / Courses / DescriptionsCOMP_ENG 356: Introduction to Formal Specification & Verification
VIEW ALL COURSE TIMES AND SESSIONS
Prerequisites
Mathematical maturity (please talk to the instructor if you are not sure what that means).Description
Introduction to formal techniques used for system specifications and verifications: temporal logic, set theory, proofs, and model checking. TLA+ (Temporal Logic of Actions) specifications. Safety and liveness properties. Real time specs and verifications.
REQUIRED TEXT: L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison Wesley. 2003.
COURSE COORDINATOR: Prof. Hai Zhou
COURSE GOALS: Correctness assurance is the most important aspect in the design of systems, especially those of life or social critical functions. “Testing can at best show the presence of errors, but never their absence”. Formal techniques treat a system as a mathematical object and relate its behavior with its structure through mathematical reasoning (i.e. proofs). In this course, we will study how to specify the behavior of a system formally and how to establish its correctness rigorously. With an introduction to discrete math, set theory, and temporal logic, we will study how to specify and verify systems using the TLA+ language and tools.
DETAILED COURSE TOPICS:
Week 1 Simple math and TLA specs
Week 2 Asynchronous interface specification and TLATeX typesetter
Week 3 Caching memory specifications
Week 4 Temporal logic: safety and liveness properties
Week 5-6 Model checking and TLC
Week 7 Specification and verification of real time systems
Week 8 Composing and decomposing systems
Week 9-10 Distributed systems and algorithms
COMPUTER USAGE: Students are required to download and install the TLA+ tools on their machines. They need to typeset specifications, check syntax, and check properties using TLC (a model checker for TLA+).
LABORATORY: EECS Department Workstation Lab. Accounts will be arranged if needed. The lab consists of a collection of high-speed workstations.
GRADES:
- Homework - 50%
- Project - 40%
- Class participations - 10%
COURSE OBJECTIVES:
- Understand the general concepts of formal specification and verification.
- Understand the basic concepts in temporal logic, set theory, and discrete math.
- Be able to specify a general system in TLA+.
- Be able to verify general safety properties by proofs or TLC.
- Understand system correctness as an important part of engineering ethics.
ABET CONTENT CATEGORY: 100% Engineering (Design, and Discrete Math components).