A twelve-week track on building precise models of systems and checking their properties — logic, temporal logic, model checking, process calculi, Petri nets, and timed/probabilistic models. Scope is formal modelling, using the lab's own MQTT/protocol stack only as a running example (no security/trust framing). The throughline: a model you can check beats a description you can only argue about.
The 12-week arc
1 of 12 lectures published — each a self-contained read with a slide deck and runnable workbook. Start at the first published week and work forward.
| Wk | Theme & focus | Read |
|---|---|---|
| 01 | From informal spec to checkable property start here Why a precise model catches real bugs an English spec hides | read → slides · workbook |
| 02 | Logic refresher Propositional & predicate logic as the substrate for everything after | planned |
| 03 | Temporal logic: LTL & CTL Expressing "always / eventually / until" properties precisely | planned |
| 04 | Transition systems & model checking States, paths, and automated property checking; the explosion problem | planned |
| 05 | Process calculi (CSP / CCS) Composing concurrent protocols formally | planned |
| 06 | Petri nets for distributed systems Concurrency, tokens, reachability — a natural week for an **interactive net visualisation** | planned |
| 07 | Timed automata & real-time properties Deadlines and timing, with UPPAAL | planned |
| 08 | Specifying a protocol Modelling the lab's own MQTT channel as the running example | planned |
| 09 | Safety & liveness verification "Nothing bad happens" vs "something good eventually does" | planned |
| 10 | Probabilistic model checking Reliability / QoS as quantitative properties, with PRISM | planned |
| 11 | Property-based testing Lightweight formal methods (Hypothesis): specs without full proofs | planned |
| 12 | Capstone Model and check one property of a real lab protocol | planned |
Capstone
Week 12: pick one protocol or component from the lab's stack, build a formal model of it, state a property worth guaranteeing, and check it — reporting what the model abstracts away and why that abstraction is safe.