Formal methods are mathematical systems used to model different aspects of a proposed or existing software system, and the associated tools used to verify that the models abide by desired behaviors (and avoid undesired behaviors). Unlike traditional calculus-based engineering mathematics, formal methods rely primarily on discrete mathematics and computer science formalisms such as finite state machines.
In this course we will explore the application of two such methods: Alloy, used to model and reason about structural relations in a design, and Spin, a system for modeling and reasoning about concurrency.
There is no text for Alloy; everything necessary will be presented in class. Take good notes!
For Spin, the required text is Principles of the Spin Model Checker by Mordechai Ben-Ari. Feel free to purchase this book second hand if you can find it.
Week | Session 1 |
Session 2 |
Notes |
01 (Nov 26) | Course
overview An Alloy example |
Signatures
and fields Propositions and predicates Elements, sets, relations |
|
02 (Dec 3) | Set
/ Relation operations Set / Relation predicates Set / Relation comprehension |
Homogeneous
vs.
Heterogeneous DAGs, Equivalence Relations facts, preds, assertions, functions |
|
03 (Dec 10) | Orderings Alloy misc. (e.g., let statements) Solving logic problems |
Alloy
1-hour exam (closed book) Alloy project released Static models |
|
04 (Dec 17) | Static
models (cont'd) Dynamic models |
Dynamic
Models (cont'd) Traces |
|
05 (Jan 7) | Traces Alloy wrapup |
Alloy 2-hour exam (open Alloy) |
Alloy project due by 11:59PM on the day before week 6 session 1 |
06 (Jan 14) | Promela
/ Spin - A simple example Simulations in Spin |
Spin processes; interleaving; FSMs init process; processes w/args. |
|
07 (Jan 21) | Synchronization in spin. atomic and d_step Safety & Liveness (progress) |
Linear temporal logic in Spin Model checking in Spin |
|
08 (Jan 28) | Deadlock Dining Philosophers Livelock (liveness violation) |
Spin /concurrency 1-hour exam (closed book) Spin project released |
|
09 (Feb 4) | Spin channels for interprocess communication. | Distributed systems: Byzantine Consensus (and more!) |
|
10 (Feb 11) | Expansion joint. Other examples |
Course evaluations. Course wrap-up. |
Spin project due by 11:59PM on Sunday, Feb 17, 2013 |
Finals Week | Final Exam Monday, Feb 18, 2013 from 12:30 - 2:30 |
We will use the standard RIT grading scheme to convert from percentage to letter grades. An A = 100-90, B = 89-80, C = 79-70, D = 69-60 and F = 60 and under.
We will have daily, one question, quizes at the end of every class. Quizes will be marked and will account for 1/3 of the homework and quizes component (ie., 3.33%).
Homework will be assigned on many but not all class days. Different
instructors may assign different assignments and follow a different
schedule., and you will
have until the start of the next class to complete and submit it to the
dropbox. You will have 4 days to complete each homework assignment as
shown in the following table:
HW Assigned | HW Due |
Monday |
Thursday @ 11:59 PM |
Tuesday | Friday @ 11:59 PM |
Wednesday |
Saturday @ 11:59 PM |
Thursday | Sunday @ 11:59PM |
The only way to receive an X is to fail to submit your homework on time - and it is your responsibility to ensure submissions are on time. In particular, complaints such as "I made a mistake on the due date" or "I was only a couple of minutes late" will be ignored by instructors. If homework is due at 11:59, then submit something, even if incomplete or incorrect, well before this time to ensure you receive better than an X.
Instructors may, at their discretion, adjust the raw letter grade by plus or minus (e.g., A+ or C-).
Homework solutions will be published after the due dates.
One hour Alloy closed book exam |
10% |
Two hour Alloy open Alloy exam |
20% |
One hour Spin / concurrency closed book exam |
10% |
Two hour Spin / concurrency final exam |
20% |