Fall 2007 Syllabus

CS 5383 Topics in Software Assurance: Model Checking

Instructor:             Dr. Steve Roach

Office:                    Comp 224

Phone:                    (915)-747-5727
(915)-747-5030 fax

email:                      sroach@utep.edu

Office Hours:        By appointment.

Prerequisites:        Senior or Graduate standing

Class Time:            4:30-5:50 Tuesday and Thursday

Text Book: Gerard Holzmann,  The SPIN Model Checker Primer and Reference Manual, Addison-Wesley, Boston, 2004, ISBN 0-321-22862-6.

Course Objectives: This course will provide students with the fundamentals of software model checking including mathematical logic and reasoning with attention to propositional, predicate, and temporal logic. Students will learn processes for formally defining requirements of a system and verifying properties of the system using the model checker SPIN.

Examinations: Examinations are assumed to be closed book, closed notes, in class, unless otherwise specified. I do not give make-up examinations. If you miss an examination for a legitimate reason ( such as illness, death in the family, participation in a college sponsored activity), then your (comprehensive) final examination will be counted extra to compensate for the missed work. If you miss an examination with out a legitimate reason, a grade of 0 will be recorded for that examination. If you know you will be missing an exam date due to a college sponsored activity, you may arrange to take the exam in advance.

Grading Summary: A: 90-100  B: 80-89  C: 70-79  D: 60-69  F: 0-59

                Midterm                 15%

Final                       20%

Assignments        35%

Project                    30%

General policies:

Time: This course is time intensive. You must start assignments early and work steadily to be successful. Late assignments are not accepted unless approved in writing or via email prior to the original due date.

Grading errors: I am only human. I can and will make mistakes. You have one week after graded material is returned to the class to rectify any grading errors or to argue for additional credit. After the week has passed, no changes in grades will be made.

Class Attendance and Participation: As a graduate student, you have the freedom to choose whether or not to attend class. Notice: You will find me unaccomodating if you come to my office to have me explain material covered in a lecture you did not attend. I consider the material covered in lecture highly relevant to the course and suggest that you adopt this opinion, also.

Office hours: I expect you to meet with me outside of class time to discuss the course material. My hours are by appointment. You may reach me by phone (leave a message) or by email to arrange a time. I will make every reasonable effort to accommodate you. My office policy is an "open door" policy: if the office door is open, you are welcome to come in and discuss problems. If my office door is closed, you should assume that I am not available.

I am available to assist you in solving problems, not to think or do work for you. My office hours are for helping you by clarifying material that you observe and for assisting you with problems you are encountering. You should come to my office prepared. The harder you work at it, the harder I’ll work to help you.

Incomplete: Students receive a grade of Incomplete only under extraordinary circumstances: when they have substantially completed the course work with a passing grade, but cannot finish the course for a legitimate reason. Legitimate reasons include severe illnesses and debilitating accidents. Class or workloads that are too demanding are NOT legitimate reasons.  Refer to my web page for a further discussion of the Incomplete grade.

Lecture material: You are expected to preview lecture material BEFORE coming to class, including reading the assigned material from the text book. Some material may not be in the text: references will be provided, but you are responsible for the content.

Academic dishonesty: Plaigarism is defined as submitting work under your name that was not done entirely by you for individual assignments or by your team for team assignments. (This includes taking programs from the web or cutting text from web pages and pasting them into documents, even if the source is cited. It also includes substantially copying homework assignments or programs from other students, even if they are not taking this course this semester.) Plaigarism and other unethical behavior will not be tolerated--those caught will be reported to the Dean of Students. You should be aware of the Standards of Conduct posted at http://www.utep.edu/vpfa/student_affairs/student/studindex/htm.