Glider
"In het verleden behaalde resultaten bieden geen garanties voor de toekomst"
About this blog

These are the ramblings of Matthijs Kooijman, concerning the software he hacks on, hobbies he has and occasionally his personal life.

Most content on this site is licensed under the WTFPL, version 2 (details).

Questions? Praise? Blame? Feel free to contact me.

My old blog (pre-2006) is also still available.

Sun Mon Tue Wed Thu Fri Sat
     
15
       
Powered by Blosxom &Perl onion
(With plugins: config, extensionless, hide, tagging, Markdown, macros, breadcrumbs, calendar, directorybrowse, entries_index, feedback, flavourdir, include, interpolate_fancy, listplugins, menu, pagetype, preview, seemore, storynum, storytitle, writeback_recent, moreentries)
Valid XHTML 1.0 Strict & CSS
/ Blog / Uni
Spin & XSpin: formal verification

I'm following a course called "Concurrent and Distributed Programming" (CDP). It concerns programs that run at the same time in a multiprocessor, multiprogrammed or multiple device environment. The main part of the course is proving correctness of such programs. In layman's language: If multiple things happen at once (such as lots of cars driving on a crossing), how do you prevent certain things from happening together (cars driving in perpendicular directions) without the risk of waiting forever (always letting one direction first).

Pretty interesting stuff, actually. Quite a different mindset from normal programming. I've already had some experience with this in other courses (Operating Systems, Programming), but this is more formal and actually proves that algorithms are correct. Something I like :-)

The nasty side of it is that the classes are pretty chaotic. The teacher doesn't really do a good job at explaining the stuff. Add to that that a lot of her sheets (containing very formal, non-trivial to understand code) contain stupid errors and you get a pretty lousy class.

Anyway, I've been installing spin, the validation tool used for this course. I have yet to understand what it can do, though. For now, I was able to do the first (easy) assignment by clicking around in the graphical front-end, xspin. Both are pretty easy to install. Spin is written in C and needs a simple compilation, xspin is TCL/TK and works out right away (if you follow instructions).

The bigger challenge was to make a screenshot of the application showing the simple Promela model, the output and my name. After doing the necessary resizing and converting (I had to hand in the screenshot in PDF format...), I got it done. Let's hope the classes will improve a little and this might turn out to be a fine course.

Comments
Brenda wrote at 2006-02-16 19:16

Perhaps you should give some feedback to the teacher so she'll know how to improver her lessons. Waiting around for her to find out by herself might not proove to be very useful.

Matthijs Kooijman wrote at 2006-02-17 00:40

That sounds like a nice plan, but... The thing is, how do you put that? Walk up to here saying "Your class is sucky!"? Also, I think she realizes that she's not really getting the entire message across. I might throw her an email I guess...

Brenda wrote at 2006-02-17 11:01

Well, as long as she doesn't think she's doing great, I'm sure she'll accept any help she gets. Just don't say "you're sucky" but point out what she could change to make things better. ;) And e-mail might be a good way to do it, so that not everyone will know about it.

Comments are closed for this story.

 
3 comments -:- permalink -:- 20:50
Copyright by Matthijs Kooijman