System Validation (2IW26)

Last update: September 5, 2014.

Rooms for discussion of the assignment

The meetings to discuss the assignment will take place in the following rooms in the Metaforum building.

Monday from 13:00-17:00.

08-Sep   MF5.122
15-Sep   MF3.141
22-Sep   MF3.144
29-Sep   MF3.144
06-Oct   MF3.141
13-Oct   MF3.144
20-Oct   MF3.144
27-Oct   MF3.119
03-Nov   MF3.141
10-Nov   MF3.141

Woensdag 11:00-15:30 uur

10-Sep   MF6.131
17-Sep   MF3.144
24-Sep   MF3.144
01-Oct   MF6.131
08-Oct   MF3.144
15-Oct   MF3.144
22-Oct   MF3.144
29-Oct   MF3.144
05-Nov   MF3.144

Dates of the lectures and the examinations

Classes take place at Wednesdays 1/2 hour (Aud 8) and Fridays 7/8 hour (Potentiaal 1.05). The first lecture will take place on Wednesday September 2, 2014. The exam will take place on Monday, November 3, 2014 from 13:30 to 16:30 (register before October 19, 2014). There is a possibility to retry the exam on Friday, January 30, 2015, 13:30-16:30 (register before January 11, 2015). See owinfo.tue.nl or oase.tue.nl for information regarding the location. The final date to hand in the pre-final report for the assigment is Friday, October 24, 2014. The final report must be handed in on Monday, November 10, 2014. Both the pre-final and final report must be handed in on paper. The corrected pre-final report must be handed in with the final report. The assignment and exam contribute equally to the final score. No study material is allowed to be used at the exam. A list of process axioms and equalities on modal formulas will be attached to the exam.

Literature:

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 BCF (MF 3.083) of the faculty 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. 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 (-h) flag that gives a concise description of the tool and its use. All tools can be started via the command line, and the most important tools work in the mcrl2-gui environment.

Go back