SWEN-220 Mathematical Models of Software
Spring 2175

Section 01: Mon-Wed-Fri  01:25-02:20
Section 02: Mon-Wed-Fri  11:15-12:10

Professor Bruce Herring

(01) myCourses shell
(02) 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 (Jan 15)

No Class
Mon 1/15
MLK Day
PART I - Relational (Data) Modeling

Course Introduction

Relational Model - Overview

Relational Model - Operations

[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 (Jan 22)

Last Day to
Add/Drop
Tues 1/23
Conceptual Modeling - ERD Intro

Course Registration Example
ERD Modeling Activity #1 ERD Project Available
Week 3 (Jan 29) Conceptual -> Relational Mapping
Course Registration Mapping
Normalization
Relational Model ->  Relational Database 
ERD Modeling Activity #2 :
Using the ERD solution from Activity #1 define the relational model using Relational Schema Notation (RSN).

ERD Modeling Activity #3
Week 4 (Feb 5) PART II - Structural Modeling
(Alloy)

Alloy-01 : Alloy Introduction

Relational Model - Operations (review)
Video - Hello Alloy

Alloy Activity #1
ERD Project Due
Mon - 2/5

Exam #1 : Relational Modeling
Wed - 2/7
Week 5 (Feb 12) Static Modeling
Assertions

Alloy-03 : Alloy Logic

Alloy-04 : Alloy Navigation - Join
Alloy Activity #2 Alloy Project Out
Week 6 (Feb 19)

No Class
Wed 10/4

Career Fair
Alloy-05 : Transitive Closure


Alloy-06 : Let and Functions
Alloy Activity #3
Week 7 (Feb 26)

No Class
Mon 10/9
October Break

Puzzles - Ordered & Unordered


Alloy Activity #4
Alloy Project R1 Due
Wed 2/28 - 11:59 PM

Exam #2 : Alloy Modeling 
Fri - 3/2
Week 8 (Mar 5) Alloy-08 : Dynamic Summary

Alloy-08 : Dynamic Summary
Alloy Activity #5 (Parking Garage)
Spring Break 3/12 - 3/16
Week 9 (Mar 19) PART III -  Behavioral Modeling
(SPIN/Promela)

SPIN-01a : Concurrency Introduction
SPIN-01b: Shared Mutable State
SPIN-01c: Deadlock

Java Concurrency Tutorial
Java Threading Activity

[SPIN] -  Chapters 1 & 2
Alloy Project R2 Due
Wed 3/21 - 11:59 PM

Week 10 (Mar 26)


SPIN/Promela Introduction
Modeling Concurrency
Semaphores

Slides:
SPIN-02 : SPIN/Promela Intro
SPIN-03 : Modeling Concurrency - Pt 1
A Primer on Model Checking
Video - Hello SPIN

SPIN Activity #1

SPIN Activity #2 (Ice Cream Race)

[SPIN] - Chapters 3 & 4
Week 11 (Apr 2)

Last Day to       Withdraw
Fri (4/6)
Verification in SPIN
Synchronization - Semaphores

Slides:
SPIN-04 : Modeling Concurrency - Pt 2
SPIN Activity #3 SPIN Project Out
R1 Due Mon (4/23)
R2 Due Mon (4/30)
Week 12 (Apr 9) Verification with temporal logic
[] and <>
Safety and liveness in LTL

Slides:
SPIN-05 : SPIN Verification
SPIN-06 : Temporal Logic
Sleeping Barber Problem
Read :
[SPIN] - Chapter 5
Exam #3 :
Concurrency Concepts & Promela Intro
Monday
Week 13 (Apr 16) Channels
Sending messages
Receiving messages

Slide:
SPIN-07 : Channels & Messaging
Read :
[SPIN] - Chapter 7.1-7.4
SPIN Project Model 1 Due
TBD

Week 14 (Apr 23)


Producer-Consumer Model

Additional Channels topics
SPIN Activity #4 
Week 15 (Apr 30)

Last Class
Mon 4/30
Final Review
ERD Review Activity

Alloy Review Activity


SPIN Project Model 2 Due
TBD

Final Exam Week May 2-8

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.)