4010-420 Formal Methods of Specification and Design
(Formal Methods)

Table of Contents

Synopsis
Course Texts
Schedule of Topics
Grading
Important Dates
Tools

Synopsis

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.

Texts

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.

Tentative Schedule of Topics

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


Alloy (weeks 1-5)

Spin (weeks 6-10)

Grading

Grading Scheme

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.

Homework and Quizes (10%)

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

Homework will be graded on a letter, where A = 90, B = 80, C = 70, D = 60, F = 50, and X = 0. Your final homework grade will be the average of the individual grades.

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.

Projects (30%)

There will be an individual project for both Alloy and Spin. Each project is worth 15% of your grade.

Exams (60%)

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%

Tools

Alloy

  1. Direct your browser to alloy.mit.edu. This is the Alloy community website.
  2. In the upper pain, click the Software link.
  3. In the tool list, click on Alloy Analyzer 4.1.10.
  4. Click on Download the Alloy Analyzer and related documentation here (the last sentence).
  5. Under Download Alloy Analyzer 4.2 Release Candidate, click on this jar file.
    1. This will download the jar file containing the Alloy tool and support libraries. Save this as alloy.jar somewhere on your Z drive. Double clicking the jar file will launch the Alloy analyzer.
    2. We advise you to bookmark the page alloy.mit.edu/alloy4 as there are links to lots of useful information; pay particular attention to the What's New section and the following links off this page:
      1. Alloy 4 walkthroughs and tutorials.
      2. The FAQ list.
      3. An Alloy 4 quick guide.

Spin

See the text, especially the appendices, for the components of the Promela/Spin toolkit. We will supplement this with information on using the tools when we begin the Spin material.