Syllabus in PDF    
 

Course Objectives

This course will expose students to formalisms in specifying, analyzing and verifying software systems. Petri nets, temporal logic, Z, and statecharts will be discussed. The focus is on the modeling and analysis power of Petri nets and extended Petri nets.

Textbook

There is no official textbook for this course. However, teaching notes will be distributed in the class.

Course Work

There will be 4 homework assignments, a midterm exam, a final exam and a team project.

All homework must be turned in by the due day.

Grading

Homework              40%

Project                     20%

Midterm                   20%

Final exam              20%

Withdrawal

Last date to withdraw with automatic assignment of a "W" grade: March 31, 2008.

Attendance

Attendance at classes is required. Students are responsible for all material covered and announcements made in class.

Academic Honesty

Everything turned in for grading in this course must be your own work.

By the Monmouth University policy, students found to be in violation of this rule will, at the very least, receive a failing grade in the course and may be subject to stiffer penalties. Students who contribute to violations by sharing their work with others are subject to the same penalty.

Special Accommodations:

Students with disabilities who need special accommodations for this class are encouraged to meet with me or the appropriate disability service provider on campus as soon as possible. In order to receive accommodations, students must be registered with the appropriate disability service provider on campus as set forth in the student handbook and must follow the university procedure for self-disclosure, which is stated in the Guide to Services and Accommodations for Students with Disabilities. Students will not be afforded any special accommodations for academic work completed prior to the completion of the documentation process with the appropriate disability service office.

 

Topics Covered

The following is the tentative lecture schedule for this course. Dates and topics may change during the semester.

Date	Lecture
1/24	Introduction to formal methods
1/28	Petri nets graphical representation
1/31	Modeling exercises
2/04	Modeling exercises
2/07	Mathematical definitions
2/11	Reachability, boundedness, safety, liveness
2/14	Reachability tree and reachability graph
2/18	Coverability tree and coverability graph
2/21	Incident matrix and state equation
2/25	Place invariant and transition invariant
2/28	Siphon and trap
3/03	Review
3/06	Midterm
3/17	Petri net reduction
3/20	State machine, marked graph and free-choice net
3/24	High-level Petri nets
3/27	HLPN modeling exercises
3/31	Timed Petri nets
4/03	Minimum cycle time
4/07	Project
4/10	Project
4/14	Stochastic Petri nets
4/17	System performance evaluation
4/21	Temporal logic
4/24	Statecharts
4/28	Z specification language
5/01	Project presentation
5/05	Review