Course analysis: 2G1516 Formal Methods, {D,IT}4, SEDS Masters, HT05
Mads Dam, 2006-01-31
Course Data
2G1516 given for D, IT, SEDS masters (also 1 student from the EMIS masters program)
Period and year: Period 2, HT05
Number of credits: 5 pts (2G1516), written examination (3pts), 3 labs (2pts)
Course responsible: Mads Dam
Lecturers: Mads Dam
Assistants, recitations and labs: Mika Cohen
Number of lectures: 12x2 hours
Number of recitations: 12x2 hours
Number of labs: 3
Literature: Peled: Software Reliability Methods
Web page: www.imit.kth.se/courses/2G1516
Quantitative data
Number of registered students:
13 (= number of students completing or attempting at least one lab or exam)
Program distribution: D: 7, SEDS: 3, IT: 1, EMIS: 1, PhD students: 1
Number of "defectors" (students that selected the course or appeared in some activity but didn't register): 8
Number of student sitting final exam: 13
Number of students passed first time: 9
Degree of performance: 69% (ratio of students passed main exam in first attempt vs number of students following the course)
Degree of examination: 69% (ratio of students passed all course requirements during period 1 vs number of students following the course)
Examination statistics: U: 31%, 3: 8%, 4: 38%, 5: 23%
Current course: What was new?
This was the third time the course was given. During 04-05 the course was given as an obligatory course for the newly established SEDS masters program. Since this was not the case in this year, in 05-06 the number of students was smaller, and the students were generally better motivated and prepared for the topic. This allowed us to cover somewhat more material and keep a somewhat higher speed throughout. The main difference in relation to the 04-05 version were that the section on theorem proving was dropped in favour of increased emphasis on process algebra, in particular reinstating the concurrency workbench lab. This change was made to reflect the focus of the other material covered in the course (mainly automated methods for mainly concurrent/distributed systems) a bit better. Another change was the relocation of the course from Kista, period 1, to Valhallavägen, period 2.
Comments
Student representatives of the course committee did an excellent summary of the course enquiry, attached below.
Overall, the 05-06 installment of the Formal Methods course was successful in the sense that the different course elements were completed in a good way, the students found the course worthwhile and interesting, and most students met the goals set out in the course pm.
Main issues:
Students from D and SEDS have widely differing backgrounds, and in SEDS students in particular have difficulties with the mathematically oriented parts of the course. Also the course would benefit from more familiarity with c.s. topics such as automata and basic logic and semantics (prerequisites). Next year the course will swap period with the semantics course which will probably remedy this issue to some extent.
Tools used in the labs create some frustration, in particular the ESCJava tool. Important in coming years to streamline use and installation more which can be painful. The quality of the ESCJava(2) tool should improve over time as this is subject of ongoing development. The lab itself has a somewhat different nature from the other two labs which are better aligned with the underlying course material. There are various options for improving this lab, by expanding it to cover more comprehensive treatments of invariants, and/or by replacing the priority queue example by another, sllightly more ambituous, piece of code. The main rationale for including an ESCJava lab - to demonstrate a more scalable approach to verification - remains valid.
The textbook is not optimal - there is lack of exercises though by now we've worked round this to a large extent, and also it is not particularly well written. A good alternative would be the textbook by Ryan and Huth which we should consider for next year.
More exercises with reference answers might be useful. Currently these exist only for old exam questions - the answers there are often terse.
The modelling aspect is covered relatively little in comparison with verification and algorithms. It might be useful to replace one of the protocol verification labs - probably the ccs/cwb lab - with a more modelling oriented lab, e.g. some workflow or production line/robotics type of example.
The exam is a 5 hour written exam consisting of 6-7 questions, graded on a 100 point scale, this year divided as follows: 0-49: U, 50-69: 3, 70-84: 4, 85-100: 5. An alternative would be a take-home exam. For this course the main objective of the exam is to check the students grasp of the range of basic topics covered in the course - for that purpose the current exam format seems quite well suited.
Course Committee and Course Evaluation
The course committee consisted of M. Umair Tajammul, O. Kafray of SEDS, and Oscar Tengwall of D. The committee met once during the course, no written minutes. The students summarized the course enquiry, attached.
Preparation for Next Years Course
Consider changing textbook to Ryan and Huth. This will have consequences throughout the course.
Labs should be given routine revision. Consider replacing the CSMA/CD example with a more modelling oriented example, type production line
Consider effects of swapping period with the semantics course, in particular in relation to Hoare logic.
ECS/Java exercises should possibly be introduced
Mads Dam, Jan 31, 2006
2G1516 - Course Evaluation
General overview:
In general everyone seems to be very happy with the performance of Mads Dam and Mika Cohen. The only negative comments that were found in this evaluation was that the tools used in the lab assignments were not that good. The most concrete suggestions raised were:
- Try to publish more exercise solutions on the web pages.
- Many student found the Spin and ESC lab tools to be annoying. A big part of the time spent with these labs seems to have been spent on getting the tool to behave correctly.
Lectures
1 Worst
|
2
|
3
|
4
|
5
|
6 Best
|
Q1. Which percentage of lectures did you attend?
Most students have attended regularly (4.5).
Q2. How useful are the lecture notes?
The lectures notes were generally useful (5.0).
Q3. How is the lecturer pedagogically?
The lecturer is pedagogical (4.75).
Q4. How useful are the lectures?
Everyone seems to have found the lectures useful (5.0).
Lecturer & Lab Assistant
Q5. Is the lecturer enthusiastic and motivated?
In general the students think that lecturer was very motivated and enthusiastic (5.5).
Q6. How well does the lecturer answer questions?
Almost some the students think that the lecturer answered questions very well (5.5).
Q7. How friendly and helpful is the lecturer during breaks, in Emails, etc?
The lecturer was quite friendly during breaks and emails (5.5).
Q8. Does the lecturer use available tools appropriately?
One student suggested that the lecturer should have demonstrated more tools in the class (4.0).
Q9. Did you get enough help from lab assistant?
The students were generally happy with lab assistant (5.0).
Labs/Assignments
Q10. Labs
Spin Lab
Mostly students found the lab difficult and required a long time to complete the lab. Fortunately many student also found the lab to be very interesting (5.5). , highly relevant to the course, very useful for understating the course. However, mostly students did not grade suitability of tool very highly (3.5).
ESC Java Lab
This lab was generally considered to be the easiest / least time consuming lab. Some students found the lab very interesting and some students did not find it that interesting (3.0). They graded the lab moderately useful for understanding the course (3.5). Students found the lab fairly relevant but the tool was not graded very highly and most students do not appreciate the tool (3.0).
Lab3 (CCS)
Most students found the lab difficult and time consuming with the exception of two students who found it easy. Almost all students found the lab very interesting (5.0), stimulating (5.5), very relevant (5.5) and very useful for understanding (5.5). The tool although not top marked was more useful than the other two tools (4.0).
Overall Course
1 Worst
|
2
|
3
|
4
|
5
|
6 Best
|
Q11. How well did the course goal show at the beginning of the course?
Well (5.5).
Q12. Do you have all prerequisite knowledge for the course?
Most people had sufficient prerequisite knowledge (5.0).
Q13. How meaningful do you consider the course?
Quite meaningful (5.5).
Q14. How difficult do you consider the course?
Difficult (5.0).
Q15. How is the course altogether?
Very good (5.0).
Q16. How useful are the course web pages?
Very useful (5.0).
Subjects Covered by the Course
Q17. How well did you find following elements of the formal methods subject covered by the course?
Formal Modelling
All students agree that it should be part of the course even though the difficulty level was found to be high. This part was found to be well covered and very interesting (5.0).
Verification analysis
All students agree that it should be part of the course even though the difficulty level was found to be medium (4.5). This part was found to be well covered and very interesting (5.0).
Theoretical underpinnings
All students agree that it should be part of the course. The difficulty level was high (5.0) while it was well covered and interesting (4.5).
Applications
All students agree that it should be part of the course. The difficulty level was easy in most cases. Some student felt that this part should have been covered better. Most students found it very interesting (5.0).
Tools
All students agree that it should be part of the course. As with the applications some students thought that the tools should be covered better. Most students found it very interesting (5.0).
Q18 .Do you expect you will find use of the subject in your future career?
Most students think that it will be useful, though it may not be immediate.
Q19. Any general comments about the course?
General comments
One of the most interesting courses I have taken. Great lectures. I don't go to lectures if I think 2 hours of reading will give as much , but in this course I would not want to miss a minute.
Semantics course should go before this course to lessen the emphasis on Hoare-Floyd.
Fun and challenging.
Exercises
It would be better if the solutions to the exercises would be published on the course webpage, as we were not able to solve all the exercises in exercise sessions.
There should be thorough written solutions from exercise sessions.
More exercises with solutions to be added to be well prepared for the exams.
Labs
CCS lab can probably be extended – there can be another lab to verify congruence etc.
More checkpoints to be added in spin lab so that they know that they are on the right path.
Spin/ESC Java labs were frustrating and only CCS actually helped improving understating.
Literature, references and course web page
One student says that the book is uneven. I think he means that it’s organized quite differently from how Mads’ had organized the course.
Few references to Owicki-Gries (not even in book).
The course Web page is annoying, the link names don’t necessarily correspond to content inside and slides are not numbered chronologically.