ANALYSIS OF SOFTWARE ARTIFACTS

17-654 -- Spring 2000

Somesh Jha School of Computer Science, Carnegie Mellon University

The purpose of the course is to teach analysis techniques for artifacts that arise during various phases of the software process. Some of the topics that are covered are model checking, object modeling, testing metrics, and statistical methods. Focus of the course is on fundamentals.

Time and Place:

Tuesdays and Thursdays 6:30-7:50pm in SEI A104.

A detailed schedule for lectures and homeworks can be found here [PS, PDF].

Instructor:

Somesh Jha (sjha@cs.cmu.edu)

Office: Wean 3112 (Phone: 412-268-5544)

Teaching Assistant:

Joao Pedro Sousa (jpsousa@cs.cmu.edu)

Office hours: TBA.

Textbooks:

We will distribute detailed class notes. See the Class Notes page.

The following text book will be required for second half of the class. Please buy it from your favorite online publisher.

Statistical Methods in Software Engineering (Reliability and Risk), N.D. Singpurwalla and S.P. Wilson, Springer-Verlag, New York, Inc.

Announcements and Questions and Answers:

This page will contain general announcements related to the class.
Questions and answers of a technical nature related to the lectures and homeworks.

Grading and Homework Policy:

Homeworks will account for 50% of your course grade.
Midterm and final will each be 15% of your course grade.
Project will be worth 20%.
Students will NOT be allowed to redo homeworks.
However, we will take BEST six out of eight of the regular homeworks to compute your grade.
Regular homeworks exclude the one mini homework.
For every two days you are late ten percent will be deducted from your homework score.
Homeworks must be done individually. Cheating and/or plagiarism will not be tolerated. This means that all of the work you turn in must be your own. If a student is suspected of cheating, the suspected actions will be reported to the University for investigation and possible disciplinary action. Consult the University's Policy on Academic Integrity published in the Student Handbook for further details.
Homework assignments may be down-loaded off of the Homework Assignments page.

Suggestions/guidelines for project:

Projects have to performed in a group of 3 to 4 students.
Here are the suggestions/guidelines for choosing a project.
Guidelines for project presentation and report.

Useful Links:

The model checker NuSMV.
Note:NuSMV is only available for Solaris and Linux. If you want to use SMV on NT, download the CMU version of SMV. However, use the documentation provided with NuSMV. It is much better than the old documentation.
Relational formula checker Ladybug.
A tool for checking Alloy specification Alcoa.
Oxford formal methods page.