CS 745/845: Formal Specification and Verification of Software Systems
(Coordinator: Michel Charpentier)
Focuses on the formal specification and verification of reactive systems, most notably concurrent and distributed systems. Topics relevant to these systems, such as nondeterminism, safety and liveness properties, asynchronous communication or compositional reasoning, are discussed. We rely on a notation (TLA^+^, the Temporal Logic of Actions) and a support tool (TLC, the TLA^+^ Model Checker). Prereqs: CS520 & CS659.
Course Topics and Student Outcomes
Models & abstractions (1):
Formal specification, program correctness, semantics of parallelism, safety and liveness, transition systems, symbolic logic and formal proof, induction, variants and invariants, temporal logic.
Seven homework assignments (20%), one project (30%) and two exams (50%).
Formal specification and verification:
- implementation vs specification
- functional correctness, typical properties (precondition, postcondition, invariants, termination)
Reactive systems as state transition systems:
- reactive systems vs transformational systems
- system states, initial states, state transitions, behaviors
- linear-time temporal logic (LTL), safety and liveness
- formal definition of correctness
Modeling of reactive systems:
- state predicates
- state modeling using sets and functions
- sequentiality, parallelism, nondeterminism, atomicity
- weak and strong fairness
Reactive systems in TLA^+^:
- state transitions as binary predicates
- stuttering and termination
- "next-state" predicates as disjunctive formulas
TLA^+^ syntax and semantics:
- sets and functions in TLA^+^
- tuples, sequences and records as functions
- quantifiers and set builder notation
- finite sets and cardinality
- $\land$ and $\lor$ in bulleted lists form
System properties in TLA^+^:
- $\Box$, $\Diamond$ and $\leadsto$ properties
- state-based and action-based properties
- correctness as logical implication
Model checking with TLC:
- Explicit-state model checking
- using TLC, configuration files
- limitations of TLC
Proving properties in TLA^+^:
- proving action properties
well-founded sets (variants),
WF1rule, Lattice Rule
- inductive invariants,
- Leslie Lamport. Specifying Systems: The TLA^+^ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2003. ISBN: 0-321-14306-X.
- Leslie Lamport. The Temporal Logic of Actions, ACM Trans. Program. Lang. Syst., 16(3):872-923, 1994.
Additional (for a discrete math refresher):
- James L. Hein. Discrete Mathematics, Jones and Bartlett Computer Science, 2003, second edition. ISBN: 0-7637-2210-3.