This course is dedicated to teaching the principles and application of the following tool-supported formal specification methods:
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. (Note: our materials use an earlier version of Alloy (Alpha 1.1) rather the most recent version, because when we started this version of the course in January 2002, the documentation for the older version was more complete).
We are covering aspects of UML due to its current popularity. The USE tool is very robust and 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.
In summary, these methods span the development process ranging from high-level semantic modeling (Alloy), to system architecture design (USE), to coding and debugging (ESC/Java).
No course is perfect. This one reflects our own personal biases. It continues to change and be updated as new methods are introduced and as trends in software development change. There are other methods that we have covered in the past that are quite interesting and useful. For example, we have previously covered the Z method (using various type-checkers and animators available for Z) and the Java Modeling Language JML, and it would be nice to consider related tools such as Daikon and Houdini.
We appreciate suggestions/pointers for material to cover, and for improving the presentation of the material.
You can read the rest of the text below to learn more about the organization of the course and available material. Or, you can go directly to an example course schedule (with linked slides, lectures, etc) -- this link reflects the contents of the student distribution.
The link to download an archive of entire set of materials is given at the bottom of this page. Please read the rest of the text below before downloading, as it describes some potential restrictions on the use of the streaming video lectures.
Course format: The materials in this course are presented to graduate students (primarily Master of Science and Master of Software Engineering students, with only a few PhD students) across a 15-week semester. The course is also offered through KSU's distance learning program. The on-campus section usually contains 50-60 students, whereas the distance learning section usually consists of 5-10 students from industry. Our Master of Software Engineering program (for which this course is required) is often used as a "bridge" program meaning that many of the students have undergraduate degrees in other disciplines (usually some form of engineering) and have taken a compressed series of remedial courses to prepare for computer science graduate work. Practically speaking, this means that a significant number of students in this course do not have a strong background in logic, formal semantics, or even mathematics. This does influence our decisions regarding course content. We like having Alloy in our first module because the Alloy tool gives students feedback as they learn (or recall) basic principles of first-order logic.
In past semesters, live lectures were given to the on-campus section twice a week in 1.5-hour sessions. We are not fans of the often-used distance learning format where live on-campus lectures are recorded and replayed for distance students, because we believe it results in a less than optimal experience for both sections. In this latest version of the course, we decided that we would rather spend the time to improve the quality of the recorded lectures and simply eliminate the live lectures -- both on- and off-campus students watched the recorded lectures. Frankly, we do not prefer recorded lectures (we think live interaction unimpeded by recording equipment is the best format), but we decided that giving both recorded lectures and live lectures would not be a good use of our time.
To compensate for the loss of live interaction in lectures for on-campus students, we added a weekly 1.5-hour lab session where the student were usually split into two sections with each of us in charge of one section. The lab session typical begins with a short (less than 10min) question time, followed by a 20-minute closed-book/notes quiz. The purpose of weekly quiz is to try to force students to keep up with the lectures and experimenting with the tools. The lectures themselves contain "exercise breaks" where students are asked to stop the lecture, carry out some exercise with the tool. After such breaks, the lecture usually picks up with the lecturer giving an assessment of what the student should have experienced if the exercise was carried out according to plan. The material for the lab quizzes is often drawn from the material used in these "exercise breaks" -- guaranteeing that if students have gone through the lectures, they will not be blind-sided by material they have never seen before in the quiz. Following the quiz, there is another question/answer time with either the quiz solution being presented or with a series of in-class exercises. The instructor distribution contains all these materials.
Given that we were pre-disposed against recorded lectures, we were surprised to find out that our students overwhelming preferred the new format. It seems that they found value in the guided examples in the lectures and being able to watch and replay the lectures at will. Furthermore, question/answer sections in the lab were longer and more relaxed than in live lectures in previous semesters (having a camera filming everything tends to make students reluctant to ask questions). Based on this feedback, we plan to continue this format in some of our other courses.
Lecture Materials and In-class Exercises: The video for the lectures is linked off of the course schedule. Technically, this video should not be available to non-KSU students but the current server allows us to bypass the KSU login (sshhh! -- don't tell anyone). You should be able to download a viewer for the video (just click on a video link and it will prompt you) -- it seems to work OK on Windows 98 and 2000. It was not working for Windows XP during the spring 2002, but this may be fixed by now. If you have a problem with the video, you are stuck -- please DO NOT contact KSU Online since you are not a paying student, and your contact will only alert them to the fact that we are by-passing their login system (pass this on to your students if they are watching the video). Frankly, although we over this video links as a resource, it's probably best for instructors using this course material to give live lectures themselves. This will avoid any legal issues with the KSU Online people. In addition, if you have a large class trying to view the online lectures, students could generate noticeable traffic on the KSU Online server. However, if you have a smaller class and you find the idea of using the recorded lectures appealing, then just go for it and we'll see what happens. We'll try to investigate a "proper" way to distribute the video in the future.
The quality of the video is not great, but it's not terrible either. In the first 3-4 weeks, there were technical difficulties with the recording system regarding the advancing the slides, so that the instructor had to step out of view of the camera to hit a button and then return into view. This was later resolved. In general, we find it somewhat painful to watch ourselves on the video. We are not movie stars, and lectures were always recorded with just one "take". In addition, we sometimes stumbled through recordings because they were often recorded after we had stayed up late into the previous night working. In any case, it is almost certain that other instructors will want to give their own perspective on the lecture material rather than have us talking, since we are sure that there are many interesting insights that we have omitted.
The lecture recordings are anywhere from 30 to 90 minutes long. If students are carrying out the in-lecture exercises (which they should!), working through some lectures may take 3 hours or more. The instructor distribution includes the PowerPoint slides for the lectures as well as sources for all the in-lecture examples.
Homework: Four regular homework assignments are included in the instructor distribution: two for Alloy, one for USE, and one for ESC/Java. There is also an extra credit assignment on Alloy operations. These assignments push the capabilities of Alloy Alpha 1.1, and one needs to use various tricks when debugging Alloy specs to obtain reasonable performance (the assignment description gives some estimates of what running times one can expect for checking various invariants etc for the assignment). We imagine that using the more recent versions of Alloy would substantially improve the performance. But not the latest version of Alloy using as different syntax (as noted in the introduction). In previous semesters, we had six assignments: one small assignment and one larger assignment for each tool. This was actually our goal for this semester, but our busy schedule forced us to scale back the number of assignments. The distribution includes the assignment descriptions, model solutions, and grading guidelines that we gave our teaching assistants.
Exams: Two exams with keys are included in the distribution. The time allocated for the mid-term exam was 1.5 hours; the time for the final exam was 1hr50min. Generally, the students complained that the exams were too long, but we still had student get very close to perfect scores. In our opinion, the exams are not technically difficult, but one needs to be quite familiar with the material to finish on time while completing all the questions correctly.
| Maintained by Matthew Dwyer and John Hatcliff |