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 believe that students may well use this tool in their design/development work in the future.
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.
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.
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 quizes.
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 quizes and the exams. You MAY NOT work in teams together on the homeworks. 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. 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)
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.
Obviously off-campus students will have to rely on the phone and email as their means of communicating with us and we'll do our best to make those interactions useful for you.
In this course, students get feedback from the instructor in two ways: (1) through comments on quizes 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, quizes, 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. When I (Dr. Hatcliff) was a student in this course at KSU, the instructor (later my PhD advisor) did the same thing. It always made me nervous, but it was good for me. Our 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.
Dr. Dwyer and Dr. Hatcliff's major research project involves developing the theory and constructing tools for verification of concurrent Java software systems. On this project (called the Bandera Project), we work with several other KSU faculty members: Dr. Michael Huth, Dr. David Schmidt, and Dr. Alan Stoughton. In our research, we collaborate with several other groups: the formal methods group at the NASA Ames lab in California, groups from Stanford and SRI labs, and the verification group at the University of Dortmund, Germany. We also work with people at the University of Massachusetts, University of Copenhagen, Denmark, and INRIA Sophia-Antipolis (Nice, France).
We also work on a projected funded by the Air Force Research Lab on tools for constructing software for embedded systems. We are working on this project with Dr. Masaaki Mizuno, Dr. Mitch Nielsen, and Dr. Gurdip Singh.
Our day-to-day research activities include supervising graduate students as the 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 activies 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. Dr. Dwyer is also co-editor-in-chief of the journal Software Tools for Technology Transfer and will be organizing the 2002 ACM Workshop on Program Analysis for Software Tools and Engineering (PASTE'2002) during this semester. Dr. Hatcliff is organizing the 2003 Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2003) which is part of the largest computer science conference held in Europe, ETAPS'2003 next year.
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.
Maintained by Matthew Dwyer and John Hatcliff