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 calculusbased 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 BenAri. 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
1hour 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 2hour 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 1hour 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 wrapup. 
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 = 10090, B = 8980, C = 7970, D = 6960 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% 