Karachi   ->   Sweden   ->   Karachi, again   ->   Dubai   ->   Bahrain   ->   Karachi, once more   ->   London and Leeds

Thursday, February 03, 2005

Assignments: Concurrent Programming and Formal Methods

One of the most famous assignments in DCS program at Chalmers is Train Control in the Concurrent Programming course. Apparently, it's a very good way of learning about critical sections and locking. It can also be extended to classical problems such as readers and writers by drawing the tracks in a different way. But the problem with the assignment is that when you apply brakes, the trains don't stop immediately. They slow down gradually and the time they take to come to a halt depends on their speed. Having the goal to run the trains at the maximum possible speed while managing to brake right before entering the critical section makes the assignment hard and, for me, very boring. It took me one day and one whole night at the university to complete it.

Another assignment that took most of the time last week was to simulate an elevator. We had to write it in Lustre. Chalmers has one of the finest teams in the world when it comes to formal methods for software. One of the Associate Professors, Koen Claessen, has hacked Luke that we use instead of the compiler from the authors of Lustre. Luke generates an HTML page from a Lustre file with all propositional logic embedded into it. It's very interesting. Another tool, KeY, also developed at the university, is used for complex automated verification of software properties.

If life and time permits, I intend to introduce some of these courses when I go back to Pakistan.