SWEN-220 Mathematical Models of Software
Fall 2171

Section 03: Tue-Thu  12:30-1:50

Professor Mike Lutz

(03) myCourses shell

Syllabus

Textbooks-

All required texts are available online through the RIT Wallace site: http://library.rit.edu/ 
Copy the title of the book into the search bar. 


Week
Topics / Sildes

Activities / Reading / Videos

See myCourses Dropbox for submission due dates.
See myCourses -> Content -> Video for video links.
Projects / Exams

Week 1 (Aug 28)

PART I - Relational (Data) Modeling

All data modeling lectures are available on Google Drive

Course Introduction

Relational Model & Relational Algebra



[Alloy]
- Chpt 1 : Introduction 
(focus on terms "abstraction" & "model")

[ERD] - Chpt 1 : Introduction

Lamport Video: first 9-10 minutes. We are not using TLA+, but we will use similar modeling tools. Focus on the  value of using models & abstractions when designing & testing software.


Week 2 (Sep 4)

Last Day to       Add/Drop 
Tues 9/5


Entity-Relationship Modeling

ERD Modeling Example: Course Registration


Data Modeling Activity #1 Data Modeling Project Available

Week 3 (Sep 11)


Conceptual -> Relational Mapping

Course Registration Mapping

Normalization

Relational Model ->  Relational Database (ITP)

Data Modeling Activity #2


Data Modeling Activity #3


Relational Database Activity #4 (ITP)


Week 4 (Sep 18)

PART II - Structural Modeling
(Alloy)

Alloy-01 : Signatures, Fields, etc.
Alloy-02 : More Propositions & Predicates




Data Modeling Project Due
Fri - 9/22





Week 5 (Sep 25)
Exam #1 : Data Modeling
Tue - 9/26
Study Guide

Alloy Activity #1
(due by end of day on 10/03/2017)
Alloy R1 Project Out
(follow this link)

Week 6 (Oct 2)
ALL Alloy Lectures

Transitivity & Transitive Closure
Teams example

Let and Functions
An Unordered Puzzle : Shoes
Shoes.als Skeleton
Alloy Activity #2
(due by end of day on 10/05/2017)

Alloy Activity #3
(due by end of day on 10/12/2017)




Week 7 (Oct 9)

No Class
Tue 10/10

October Break

Ordering & Ordered Puzzles
Ordering Module Reference
An Ordered Puzzle: Music Awards
MusicAwards.als

Ice Cream (Ordered Puzzle)
Ice Cream Solution

Alloy Dynamic Modeling

Dynamic Example : Team Trades

Alloy Activity #4
(due by end of day on 10/17/2017)
   PDF description
   Alloy skeleton


Alloy R1 Project Due
Friday 10/13/2017

Alloy R2 Project Out
(follow this link)




Week 8 (Oct 16)
Alloy Dynamic Modeling Continued

Dynamic Model Summary




Exam #2 : Alloy Modeling 
Tuesday, October 17

Week 9 (Oct 23)

PART III -  Behavioral Modeling
(SPIN/Promela)

SPIN-01 : Concurrency Introduction
Race.java

Airlock

Woolies

Java Threading Activity

[SPIN] -  Chapters 1 & 2

Alloy Project R2 Due

Friday 10/27/2017


Week 10 (Oct 30)

SPIN/Promela Introduction
Modeling Concurrency
Semaphores

Slides:
SPIN-02 : SPIN/Promela Intro
SPIN-03 : Modeling Concurrency (1)
SPIN-04 : Modeling Concurrency (2)

A Primer on Model Checking
Video - Hello SPIN

SPIN Activity #1 - Least Common Multiple


SPIN Activity #2


[SPIN] - Chapters 3 & 4


Week 11 (Nov 6)

Last Day to       Withdraw
Fri (11/10)


Deadlock
Verification in SPIN
Synchronization - Semaphores

Slides:
SPIN-04 : Modeling Concurrency (2)

SPIN Activity #3


SPIN Project Out


Week 12 (Nov 13)




Verification with temporal logic

[] and <>
Safety and liveness in LTL

AmySheldon.pml

Sleeping Barber
Read :
[SPIN] - Chapter 5
Exam #3 :
Concurrency Concepts & Promela Intro
TBD

Week 13 (Nov 20)

No Class
Thu, Fri 11/22-24

Thanksgiving 

Channels
Sending messages
Receiving messages

Slide:
SPIN-07 : Channels & Messaging



Read :
[SPIN] - Chapter 7.1-7.4


Week 14 (Nov 27)

Producer-Consumer Model

Additional Channels topics
SPIN Activity #4 

SPIN Project Model 1 Due
TBD



Week 15 (Dec 4)
Last Class
Thu 12/7


Java Messaging Systems (TBD)
Final Review



SPIN Activity #5 




Week 16 (Dec 11)



ERD Review Activity

Alloy Review Activity
SPIN Project Model 2 Due
TBD

Final Exam Week Dec 13-19

TBD


Resources:

Tools:

Disclaimer: While you are free to install Alloy and Spin on your personal computers, there may be some "quirks" based on your machine's configuration (especially SPIN on Mac's). I would strongly suggest defaulting to the lab systems for all on-line exams and testing projects and activities. All grading will be done using an SE Lab image. I will create a discussion forum in myCourses for students to share installation advice.
 
Alloy
  1. The Alloy community web site is at alloy.mit.edu.
  2. If you want to install Alloy on your own computer:
    1. In the upper pane, click the download link.
    2. Select either alloy4.2.dmg for OS X or alloy4.2.jar for Windows or Linux; in all cases you need at least Java 6 to run the tool.
  3. The documentation link in the upper pane leads to a page with several useful links (we suggest bookmarking this link):
    1. An FAQ about Alloy.
    2. A reference manual
    3. A quick guide to Alloy 4
    4. An on-line tutorial
    5. Slides from a one day tutorial.
Promela / Spin
  1. Our primary source for information on Promela (the PROtocol MEta LAnguage) and SPIN (Simple Promela INterpreter) is the text by Ben-Ari. Gerard Holzman, the creator of the system, has a book that goes deeper in to the underlying theory, but it's more than we need.
  2. A good supplemental source is on the SPIN community website, spinroot.com. This is where you can find downloadable versions of the tools for your own computers. In addition, there are tutorials and a community forum.
  3. To download jSPIN 5.0 for Windows go to Google Code and select jspin-5-0.exe
    https://code.google.com/archive/p/jspin/downloads?page=2
  4. To download SPIN for Mac go to the SPIN site and follow instructions for Mac installation
    http://spinroot.com/spin/Man/README.html

    Here are some additional Mac installation tips: jSpin for Mac and Linux

Data Modeling - Entity Relationship Diagrams (ERD)
  1. There are a number of ERD-like drawing tools available. In class, and for your own use I would suggest Lucidchart : https://www.lucidchart.com/. You will need to sign-up (free) with your RIT email address (*.rit.edu) in order to get features beyond the normal trial sign-up Lucidchart offers.
  2. Another  tool to look at is the ERD features in Microsoft Visio. Visio is installed on the SE lab machines and is available through the SE Deptartment's Academic Alliance with Microsoft: http://www.se.rit.edu/content/software-vendor-alliances (Note that Lucidchart is able to import Visio diagrams.)