A Brief History of the Instructors' Relationship to the Course

Drs. Dwyer, Hatcliff and Howell initially developed this course and taught it for the first time in Spring 2001. In that semester, they introduced Alloy, OCL/USE and ESC/Java as the primary tool-supported formal methods for the course. Previous offerings had a stronger focus on Z. Dr. Robby joined Dr. Hatcliff as an instructor of the course in Spring 2006.

We believe that the most effective formal specification methods are those that also provide some sort of automated tool support. Alloy, in particular, "brings specifications to life" by allowing designers to query constructed models via its constraint analyzer and to easily assess the impact of model refinements. In addition, Alloy has a readable graphical and textual notation and it has a very small and semantically clean core language. We believe that all these factors make it an excellent pedagogical vehicle and a tool that can be applied to realistic problems with a fairly large return on the analyst's effort.

We are covering aspects of UML due to its current popularity. The USE tool provides some very useful capabilities for reasoning about OCL enriched UML specifications.

We are including a module on ESC/Java because we wanted to include a discussion of code-level specifications. The fact that ESC/Java provides some support for automatically checking these specs is in line with our preference for tool-supported methods. Beginning in Spring 2009, we will be using Kiasan instead of ESC/Java.

No course is perfect. This course changed from the previous semester, and it is likely that it will change when it is taught again. We are always open to your suggestions for the choosing the material to cover, and for improving the presentation of the material.

How to survive in this course

We cover a lot of material in this course, and it is easy to get lost quickly if you do not keep up daily. We try to do several things to help you keep up. We provide the video lectures, lecture slides, and some supplementary notes that we write ourselves. We also post objectives that you should be able to meet at the end of each week, these objectives will be the topics of the weekly quizzes.

Besides all this there are a number of things that you should do to make sure that you are getting the most out of the course. BEFORE viewing each lecture you should read the required reading material. AFTER viewing each lecture, you should review the lecture slides (perhaps re-view the lecture) and any notes you have taken, then note any questions that are unresolved. You should bring those questions to the laboratory section. Obviously, you should review the weekly objectives to prepare for the quizzes.

Throughout the course you should do the homework as independently and as completely as possible. If you don't do the homework, you will have difficulty on the quizzes and the exams. You MAY NOT work in teams together on the homework. Of course, it is fine to give each other small hints. What is a "small hint"? Well, in general, you should not tell another student more information about your solution than you believe we would tell you about the model solution. For example, if you came to us and were having difficulty with a particular problem, we might remind you that we discussed a particular technique in lecture and refer you to some section of the lecture notes or a paper. We would NOT let you look at the model solution to see how we solved the problem. Please, don't violate this policy. It's not fair to the other students that are working independently, and you will be making things more difficult for yourself. If we believe that you are blatantly violating this policy you will receive no credit for your homework assignment, and you will be reported to the KSU Honor and Integrity System. Finally, remember that this is a 700-level course. Therefore, you may find the material more challenging and your responsibility for keeping up greater than in lower-level courses.

To give you a sense of amount of work we expect you to do to get an A in this course, we include these "ballpark" estimates of the amount of time you'll take each week (or for each assignment):

• Watching lectures and participating in the laboratory (4-6 hours per week)
• Reading (2-5 hours per week)
• Learning how to use the tools effectively (20-30 hours per tool)
• Homework (10-30 hours per assignment)
• Exams (10-20 hours of study per exam)

The third estimates deserves some further comment. As mentioned, you will be working with three tools during this semester (Alloy, USE, ESC/Java). After you have read about the languages supported by these tools and listened to lectures presenting the concepts underlying those languages and variety of examples, you will still have a ways to go before you can solve the homework assignments. You should expect to spend some time "playing" with each tool. They all come with examples that you should study, try the tool out on, and experiment with to develop an understanding of how to use the tool and what it can do. This takes a non-trivial amount of time.

One approach, which we advocate, is to work with the tool in an exploratory mode as soon as we introduce the language it takes as input. This can be very helpful in debugging your understanding of the underlying concepts and it also serves to get you over the tool usage hurdle.

If you find that you are having difficulties, don't panic, and don't despair. It is important that you come see us as early as possible so that we can take corrective measures.

How to interact with the instructor

If you have a question about the course material (or any other problem), the methods of interaction (in order of preference) are as follows:

• a personal visit during office hours
• a personal visit for which you have made an appointment outside of office hours
• an email (first choice for off campus students)
• a phone call

On matters of substance, it is almost always better to talk face to face. Sending email is appropriate in some situations (e.g., notifying us of a typo on homework, telling us that you can't access a file, asking a simple question that only requires a brief response by me). However, it is not the best use of our time if you send us a question by email that will require us to type for 20 minutes but could be answered with a few diagrams on by white-board in less than five minutes. So try to come in person during office hours. We understand that some of you will not be able to come to our office hours because of conflicts with another course. If you have conflict with the office hours, or if you have an urgent question, we can schedule another time for you.

Obviously off-campus students will have to rely on the email and phone as their means of communicating with us and I'll do our best to make those interactions useful for you.

Some other notes for interacting us

If you want to come outside of office hours because you have an urgent question, you can try that, but we have other responsibilities that we have to take care of. Therefore, we may tell that we are busy and ask you to come back at a later time.

When you have a programming/specification question, it will be helpful if you email your code and bring a print-out as well when you come and see us. That way, we can test your code and see exactly the error you're getting. When you have problems understanding a particular concept or the material in general, avoid saying things like "I'm totally lost" or "I don't understand anything". You should try to identify where you have gotten lost. So instead you should say "I understood W, X, and Y, but when you started talking about Z on slide 12, I didn't see how...." A more precise question helps us converge more quickly on the problem that you are having. Remember, as they say, part of being a good learner is being able to ask good questions.

Feedback

Feedback during the course is very important --- both for student and for the instructor. The student needs feedback to determine (1) how he/she is doing in the course and (2) how to make performance-improving adjustments. The instructor needs feedback to determine (1) how well the students are understanding the presented material and (2) how the structure, content, and presentation of the course material can be improved.

In this course, students get feedback from the instructor in two ways: (1) through comments on quizzes and exams (and by keys for homework and exams), and (2) by personal interaction with the instructor during office hours, etc. The TA grades the homework and should provide brief comments. The instructors the exams and try to provide as informative comments as time permits. Because we have a relatively large number of students in the course, it is difficult to provide detailed comments regarding proper solutions on the homework, quizzes, and exams. To make up for this, you will be always be provided with a complete key for each homework and exam. This will give you the model solution for each question.

As noted in the "How to Survive" section, you should come to see us during office hours any time you have problem (sooner rather than later). Of course, we will get feedback on how well you are understanding the material by grading the homework and exams. However, for immediate feedback, we will often call on students to answer questions during laboratory meetings. Sometimes people feel threatened by this, but they shouldn't. We do this so that both the instructor and student can determine how well the material is being understood. The goal is to have a relaxed classroom atmosphere where we carry on a dialogue: students should feel free to ask questions, and I should feel free to ask you questions to see if I am getting my point across.

Finally, instructors get feedback from you on the end-of-the-semester teaching evaluations. The instructors in the KSU CIS department take these evaluations seriously. Besides giving us vital information on how to improve the course, the evaluations are also included in our yearly reviews by the department and considered when we are up for promotion.

The teaching evaluations that include written comments are the most helpful. You should view the written comment section as an opportunity for you to justify your rankings in the preceding sections. If you have given lower rankings, it is most helpful if you explain why and give some suggestions on how to improve the course. If you have given higher rankings and like particular aspects of the course, then should note the things that you like and that you found helpful.

What do professors do besides teaching

As opposed to smaller colleges and universities that focus on only undergraduate teaching, most large state universities such as Kansas State University are more research oriented. This means that in addition to teaching, most faculty members in the CIS Department at KSU are expected to divide their time between teaching, research, and service activities (serving on departmental committees, and performing tasks that support the scientific community at large). When a faculty member is hired in this department, generally they are asked to devote fifty percent of their time to teaching, forty percent to research, and ten percent to service.

Day-to-day research activities include supervising graduate students as they develop software and write their theses, writing code and experimenting with the software tools that we are developing, writing papers to be published in scientific conferences and journals, and preparing talks about our research to give at various places. Our service activities include serving on departmental committees, serving on program committees for various international conferences (this involves reading and writing reviews for papers submitted to conferences), and serving on review panels for funding agencies that award research grants. We also do travel extensively to collaborate with research partners in academia and industry.

Because KSU encourages these research and service activities, it is expected that faculty members will travel during the semester to participate in conferences, engage in research with collaborators, etc. We try our best to make sure that traveling causes as little disruption as possible in our courses.