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.
|01 (Nov 26)||Course
An Alloy example
Propositions and predicates
Elements, sets, relations
|02 (Dec 3)||Set
/ Relation operations
Set / Relation predicates
Set / Relation comprehension
DAGs, Equivalence Relations
facts, preds, assertions, functions
|03 (Dec 10)||Orderings
Alloy misc. (e.g., let statements)
Solving logic problems
1-hour exam (closed book)
Alloy project released
|04 (Dec 17)||Static
|05 (Jan 7)||Traces
|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
Livelock (liveness violation)
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.
|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|
||Thursday @ 11:59 PM
|Tuesday||Friday @ 11:59 PM|
||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
|Two hour Alloy open Alloy exam
|One hour Spin / concurrency closed book exam
|Two hour Spin / concurrency final exam