CS 745/845: Formal Specification and Verification of Software Systems

(Coordinator: Michel Charpentier)

Catalog Description

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.

Evaluation

Seven homework assignments (20%), one project (30%) and two exams (50%).

Topics

  • 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
    • IF-THEN-ELSE, EXCEPT, UNION and CHOOSE operators
  • 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^+^:
    • inductive invariants, INV1 rule
    • proving action properties
    • well-founded sets (variants), WF1 rule, Lattice Rule

Textbooks

Required:

  • 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.