System Validation (2IW26)

Last update: November 1, 2011.

There will not be a lecture on 28 of September due to the PhD. defense by M. Atif.

Dates of the lectures and the examinations

In the 1st block in the first semester of 2011/2012: wednesday 7/8 hour (Aud 1) and fridays 3/4 hour (Paviljoen B1). In the second block there are only a few lectures on fridays 3/4 hour (Paviljoen B1). In the handout (which can be found below), it is incorrectly stated that this is on wednesdays. First lecture wednesday September 7, 2011. The exam will take place on Monday, October 31, 2011 from 9:00 to 12:00 (register before October 23, 2011). There is a possibility to retry the exam on thursday January 26, 2012, 9:00-12:00 (register before January 15). See owinfo.tue.nl for information regarding the location. The final date to hand in the pre-final report for the assigment is monday, January 9, 2012. Final report must be handed in on January 20, 2012. The assignment and exam contribute equally to the final score. The lecture notes are not allowed to be used at the exam. A list of axioms will be attached to the exam.

Literature:

Course overview .
Modelling and Analysis of Communicating Systems, J.F. Groote and M.R. Mousavi. This is an abridged version as handed out at the first lecture. Note that the handed out version has the number 2IW60 on the front page. This is an error for which I (=Jan Friso Groote) am to blame.... Another annoying mistake can be found in Figure 2.5. Here the alarm transition in the LTS at the right should be a loop.
Modelling and Analysis of Communicating Systems, J.F. Groote and M.R. Mousavi. This is the full version which is continuously being updated.
This exemplary exam provides an impression of how exams of this course look like.
For the toolset see the webpages for mcrl2.

The mCRL2 toolset

For those who want to use the mCRL2 toolset, look at the webpages. Among others, the pages allow to download the tools for various platforms and contain manual pages. For large systems Linux and Mac is by far preferable over Windows, because the compiling rewriter is not available on Windows.

All students can get an account at the notebook service centre (NSC) of the faculty (HG8.86) to use the toolset on svstud.win.tue.nl. Ask access to the directory /scratch/2iw26 where large files can be stored. This can be done by the NSC by putting you in an adequate group. Make your own subdirectory with names group1, group2, etc. If the NSC is closed more information is available at BCF (HG 8.73). In order to use the graphical tools it is necessary to log in using ssh with the `-Y' flag.

For using graphical programs from a windows machine, a X-server must be installed. For a MacOsX machine an X-windowing systems comes with the standard developers distribution (which is also required to compile the toolset). Logging at the svstud can be done using a program like ssh (secure shell).

All the programs on svstud reside in the directory /home/jfg/bin. Example files are in /home/jfg/MCRL2/examples. In case of problems contact J.F.Groote@tue.nl. All tools have a -help flag that gives a concise description of the tool and its use. All tools can be started via the command line, and most tools work in the squadt environment.

Go back