CSSE 373 – Formal Methods in Specification and Design

General course information

Prerequisites:

CSSE 230 – Data Structures and Algorithm Analysis

MA 275 – Discrete and Combinatorial Algebra I

Meeting times and places:

Catalog Course Description:

Introduction to the use of mathematical models of software systems for their specification and validation. Topics include finite state machine models, models of concurrent systems, verification of models, and limitations of these techniques.

Course Staff

Instructor

Nadine Shillingford

Assistant Professor of Computer Science and Software Engineering

Email: shilling@rose-hulman.edu
Office phone: (812) 877-8384
Office address: Moench F-203
Home page: http://www.rose-hulman.edu/~shilling
Office hours: Please stop by whenever. If my door is shut, just knock.

Teaching Assistants

Andrew Siegle, siegleal -at- rose-hulman.edu

Chris Covert, covertcj -at- rose-hulman.edu

Text

Required text:

Book Cover Image

Software Abstractions: Logic, Language, and Analysis
Daniel Jackson

ISBN 978-0-262-10114-1
Publisher: The MIT Press
Copyright: 2006

Learning Outcomes

Students who complete this course successfully should be able to:

Electronic Distraction Policy

I do my best to keep class interactive. But I recongize that sometimes it is hard as a student to stay focused on the class. When I was a student I tended to doodle in the margins of my notebook. With laptops in class, there are many more ways to become distracted. Unfortunately these distractions are much more pernicious, since it is very easy to get drawn into things like Twitter or Flash games.

I strongly encourage you to turn off IM and email software and only use other software for things directly related to class. If you choose to use non-class-related software during class, then please sit in the back row. Doing so will prevent your classmates from being distracted by what is on your screen. Failure to do so may result in a penalty grade for the course.

Grading

Grading Mechanisms

The learning objectives for this course are listed above. I’ll be using various mechanisms to measure your progress against these learning objectives. Among these are:

Grading Weights

The table below gives the relative weights for each of the grading mechanisms.

Mechanism Weight
Exam 1 16%
Exam 2 16%
Exam 3 8%
Homework 20%
Quizzes 10%
Project 30%

I will drop your 3 lowest quiz grades.

I reserve the right to make small adjustments to this plan, with appropriate notice. All work will be graded both on correctness and on style; after all, your eventual customers will do the same.

Late Work

Late homework will not be accepted, with the following exception:

Each student will be given 3 free “late day excuses”. You may use these to “purchase” a 24 hour extension on a homework assignment. The maximum extension on any one assignment is 24 hours. You may earn additional late day excuses by turning assignments in early. Any assignment turned in more than 24 hours before the deadline will earn one late day excuse. Late day excuses may not be applied to the project milestones. To use or earn a late day excuse you complete the Late Day Survey on ANGEL at the time you submit your solution. On group homework, all members of the group must submit the Late Day Survey.

Lost or Corrupted Files

You are expected to backup your files regularly. If you are unable to turn in an assignment on time because of a lost or corrupted file, then you must either complete it and turn it in late, subject to the Late Work policy above, or else turn in the most recent (uncorrupted) version that you have, subject to points off for any errors or incompleteness.

Integrity

Recall the Institute policy on academic misconduct:

“Rose-Hulman expects its students to be responsible adults and to behave at all times with honor and integrity.”

Exams and homework will be done on an individual basis. The simple rule of thumb for individual work is:

Never give or use someone else's code or written answers.

Such exchanges are definitely cheating and not cooperation. The departmental statement on academic honesty has more detailed advice.

Plagiarism or cheating will result in a negative grade of the same magnitude as the points possible for the assignment or exam. For example, cheating on an exam worth 100 points would result in a score of -100, roughly equivalent to getting zero on two exams. Egregious cases of cheating will result in a grade of “F” for the course. More importantly, such dishonesty steals your own self-esteem. So don't cheat.

If you sincerely believe that certain problems are too much busy work, then please bring it to my attention.

Collaboration

You are encouraged to discuss homework, and other parts of the class with other students. Such discussions about ideas are not cheating, whereas the exchange of code or written answers is cheating. However, in such discussions of ideas, you should distinguish between helping and hurting yourself and the other student. In brief, you can help the other student by teaching them, and you can hurt them by giving them answers that they should have worked out for themselves. The same applies to tutoring and getting help from the instructor.

“Hurtful help” most commonly occurs in giving away a key idea needed to solve a problem. For example, suppose you have studied a programming problem for an hour or so, and finally found that the key to the solution is to use a helping procedure you call “critical”. Your friend, after working on the problem for 15 minutes, says “I just can't see how to do this” and you say “try using a helping procedure called ‘critical’. ”

Although it takes more time, your friend will learn more if you say something like: “How are you approaching the problem, what's your plan?” (knowing that if your friend is not planning, no helping procedure will be found). If your friend hasn't planned, you should let them do it; if they have trouble planning, tell them to think about problems discussed in class that were similar, etc. If, after planning, your friend still hasn't found helping procedure 'critical', you should say something more direct like, “what helping procedures do you have?” or “how do these helping procedures help you get closer to the solution?” or “can you solve part of the problem?” The idea is to guide the other person's thinking process.

Perhaps a more common way to fall into the hurtful exchange of giving away the key idea is when you're talking over a problem that no one knows the answer to yet. Once one of you comes up with the key idea, it is tempting to blurt it out, impressing the others with your brilliance. If this happens, you should write “developed in cooperation with ...” on your solution. (Note that this disclaimer cannot be used to get away with cheating, but we're not discussing exchanging written code or answers.) It would be better for the one who comes up with the key idea say “I have it, but now I can't tell you what it is” and then try to guide the others to the solution as described above.

If you use reference materials (other than the course text) to solve a problem, please give a citation. Similarly, if you discuss a solution with another student, give credit where credit is due by making a note such as “the following idea was developed jointly with Alyssia P. Hacker,” or “the following idea is due to Ben Bittwiddle.” You cannot be charged with plagiarism if you cite in this way. (However, don't expect to excuse cheating with such a citation. That is, you cannot exchange code even if you say it was developed in cooperation with someone else. Cooperation refers to the exchange of ideas, not code or written answers.)

Syllabus developed by Curt Clifton, based on earlier work by Mark Ardis and Gary T. Leavens.