[HD] EECS3342 F26 - 2026-10-20 (Tuesday) - Lecture 10

Overview

Jackie Wang introduces the bridge-controller case study for EECS3342 and explains how correct-by-construction development uses a sequence of increasingly detailed models rather than one unmanageable model. The course will build through M0, M1, and M2, distribute requirements across those refinements, and use proof obligations to establish properties such as invariant preservation; the lecture develops M0’s abstract car-count model and shows how unguarded events can violate its capacity invariant.

Key takeaways

Correct-by-construction development controls complexity by building a chain of models, with each refinement adding detail only after its proof obligations are discharged.
In the bridge-controller design, M0 models island and bridge as one compound with car count N bounded by capacity D; it deliberately leaves the mainland count unspecified.
The bridge requirements are staged: M0 handles bounded car counts, M1 adds mainland-to-island structure and one-way travel, and M2 adds traffic-light behavior and the assumption that drivers obey red lights.
A model’s state space is the set of variable and constant valuations satisfying its typing constraints and invariants; more concrete models generally have larger state spaces.
With D = 2, unguarded ML out events can take N from 0 to 3 and violate N ≤ D, showing why event guards are necessary for safety.
To disprove the claim that all executions preserve an invariant, it is sufficient to exhibit one valid witness trace that reaches an unsafe state.

Chapters

0:00 EECS3342 Schedule: Lab 3, Written Test 1, and Review Session

Lab 3 has been released; students can use the lab room, but TAs will not attend, and Adnan can answer lab questions by email or a brief Zoom meeting.
Written Test 1 is scheduled for October 28 and covers the pre-reading-week mathematics review, not the bridge-controller material.
The test will be mostly multiple-choice with some short written responses; Jackie Wang recommends reviewing labs, slides, concepts, and the provided practice guide.
The class agrees on an online review session for Sunday at about 5:30 p.m.; Jackie plans to post a recording of the practice-question walkthrough and send a Zoom link.

7:07 Bridge-Controller Course Roadmap and Formal Verification Topics

The remaining seven weeks will apply the course mathematics to a simplified but demanding bridge-controller case study.
The roadmap includes requirements documents, Event-B contexts and machines, formal safety properties, axioms, invariants, and proof obligations.
Refinement is introduced informally as adding detail to a model; its formal treatment will require proof obligations for properties such as invariant preservation and deadlock freedom.
Written Test 2 will cover the bridge case study and provide the inference rules used in class; the cumulative final exam may require students to prepare their own reference sheets.

10:37 Correct by Construction: From Abstract M0 to Concrete Models

A correct-by-construction system is represented by a sequence of models, M0 through MN, rather than a single all-purpose model.
A single “Superman model” is impractical for a complex system because its many variables, details, and properties are difficult to construct and verify together.
M0 is the simplest, most abstract model, containing the least detail; later models become more concrete by adding information.
The final model should be close enough to an implementation that its invariants, guards, and event actions can inform C functions or Java methods.
The bridge-controller case study will use three models: initial model M0, first refinement M1, and second refinement M2.

18:35 Refinement Relations, Transitivity, and Proof Obligations

For successive models MI and MJ, MI is refined by MJ, or equivalently, MJ refines MI; MJ is more concrete and contains more detail.
Refinement can be understood transitively: if MY refines MX and MZ refines MY, then MZ also refines MX.
The practical strategy is to distribute system properties across models and accumulate detail, rather than placing every requirement in one model.
To establish that MJ refines MI, a collection of proof obligations must be discharged; the class will introduce sequent calculus and inference rules for proving them.

24:40 State-Space Size Grows as Models Become More Concrete

A model’s state space consists of possible valuations of its variables and constants that satisfy its constraints.
Adding detail makes a model more concrete and generally increases its state-space size; equivalently, decreasing abstraction tends to increase the number of configurations.
Constraints include typing rules, such as requiring a variable to be a natural number, and invariants that express safety properties, such as a bounded bank balance.
The exact state space also depends on the constraints, so a contradiction could make it empty even when many variables are present.

29:25 Bank-Account Valuations Show Why Proofs Replace Enumeration

The example uses positive constants C and L for a credit limit and upper limit, plus an accounts partial function mapping IDs to balances.
A valid valuation must satisfy both typing constraints and the safety condition that each account balance falls between the specified limits.
An empty accounts function is one valid configuration, but other valid configurations can include accounts such as Bill with a balance of 5,000.
Because the possible valuations are effectively too numerous to enumerate, proof obligations are used to verify general properties across the state space.

36:27 Bridge Requirements Assigned Across M0, M1, and M2

The bridge controller is a reactive system involving traffic lights, sensors, and actuators, although the course focuses on the first two refinements.
M0 starts with requirement 2: the number of cars on the bridge and island must be limited.
M1 adds requirements 1 and 3: the system controls traffic between mainland and island, and the bridge permits travel in one direction at a time.
M2 adds environment constraints 1, 2, and 3, including two red-or-green traffic lights and the assumption that cars obey red lights.
Sensor and actuator requirements 4 and 5 are part of the broader requirements document but are not planned for coverage in this course.

44:26 M0 Abstraction: Treat the Island and Bridge as One Compound

The full system has a mainland, bridge, island, and two traffic lights, but M0 intentionally omits those internal distinctions.
M0 treats the island and bridge together as an “island-bridge compound,” like viewing the system from so far above that the bridge cannot be distinguished.
Its variable N counts all cars in the compound without recording how many are on the island versus on the bridge.
For example, 100 cars on the island and 3 on the bridge are represented by N = 103; M1 will add detail that M0 leaves out.

51:16 M0 Context and Machine: Capacity Constant D and Invariant N ≤ D

The M0 context defines D as the maximum number of cars allowed in the island-bridge compound and constrains D to be a natural number.
The machine defines variable N as the current aggregate number of cars in that compound.
The machine invariants include N’s type and the safety condition N ≤ D.
Axiom and invariant labels use the model number and an item number, such as axm0_1 or inv0_1, to identify statements systematically.
The number of cars on the mainland is unspecified in M0; only the compound’s count is bounded.

57:25 M0 Events ML Out and ML In Have No Guards

ML out represents a car leaving the mainland and entering the island-bridge compound, so it increments N by one.
ML in represents a car entering the mainland from the compound, so it decrements N by one.
Neither event has a guard, which means both are always enabled regardless of the current value of N.
Unrestricted increments can exceed capacity, while unrestricted decrements can make N negative, so guardless events can threaten the M0 invariants.

1:02:04 Trace Demonstration: Four ML Out Events Break the Capacity Invariant

With D = 2 and initial N = 0, the invariant N ≤ D initially holds.
Repeated ML out events produce N = 1 and N = 2, both safe states, then a fourth total increment reaches N = 3.
At N = 3, the condition 3 ≤ 2 is false, demonstrating an invariant violation caused by an enabled event.
A single ML in from N = 0 would also produce N = -1, violating the intended nonnegative count.

1:06:46 Correctness Quantifies Over Every Valid Event Trace

A valid trace is a sequence of events that are enabled at each step; system correctness requires every such trace to lead to states satisfying the invariants.
Because correctness is universal, one counterexample is enough to disprove it.
The sequence of ML out events reaching N = 3 with D = 2 is a witness trace showing that the current event design is unsafe.

1:09:41 Preparation for Thursday: Review M0’s Static and Dynamic Structure

Before Thursday, students should review the M0 abstraction diagram and distinguish its static elements, such as constants and invariants, from its dynamic events.
The next session will manipulate the model and introduce proof reasoning for its properties.

Transcript excerpt

0:05 All right, good to see everybody again. So, hopefully you had a reading week, good reading week, and had a good rest. We got seven more weeks to go, and then we can definitely start a new topic. No more math review, but we're going to apply the math into some interesting case study. Most likely we're going to spend the rest of the semester building a bridge. Of course, not a real bridge, like a simplified version. It's kind of like a very demanding case study. Um today I'm going to cover some background, uh context, and also road map about the case study, and then starting from Thursday, we're going to dive into the technical part for the building the bridge, right? It's a just a little uh case study for us to see how useful the mathematics can be in some scenario. But, we'll get to it, okay? Before we actually start, I would like to

0:52 uh mention something here. Uh let's look at the uh semester calendar very quickly just to see where uh what we can expect in the remaining part of the semester. We are still more than halfway, right? Somehow the reading week was a little bit earlier this week uh this year. Okay, we're now the 20th of October, lecture number 10. We're going to start today. And your lab number three has been released uh released just earlier this afternoon. Uh I just like what I announced today. So, for tomorrow, you're still welcome to come to the lab session to work on your lab, but the TAs won't be there. They are assigned other jobs to do, but Atnem uh on the eClass, you can see his uh email there. Just reach out to him. He's going to help you about uh lab three or

This is the start of the transcript. Save this video free for the whole transcript, searchable and time-coded.

Related notes

Summary, takeaways, and chapters were generated by AI from the video's transcript and may contain errors. The video belongs to its creator, Jackie Wang.