System Validation (2IW26)
Last update: November 1, 2010.
Teachers in Eindhoven: J.F. Groote and M.R. Mousavi.
Lectures in the second quartiel will take place on thursdays!!
The lectures in the second block will take place in Auditorium 6 on Thursdays (1st and 2nd hour). This
is correctly stated on http://owinfo.tue.nl. But it is incorrectly
stated in the handout, which in incorrect form can also be found below.
Extra lecture will take place in Aud 2
The extra lecture
will take place in Auditorium 2
on Wednesday, October 27, at 10.45 (3rd and 4th hour).
This lecture will be devoted to answer questions and exercises put forward
by the audience.
Dates of the lectures and the examinations
1st block in semester 2010/2011, wednesday 3/4 hour (Helix 1) and
thursday 1/2 hour (AUD6). In the second block the lectures
are only on wednesdays 3/4 hour (Helix 1).
First lecture wednesday September 1, 2010.
The exam will take place on thursday November 4, 2010 from 14:00 to 17:00 (register before
October 17, 2010).
There is a possibility to retry
the exam on thursday January 17, 2010, 14:00-17:00 (register before January 9). 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 3, 2010. Final report must be handed in on January 14, 2010.
The assignment and exam contribute
evenly 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.A. Reniers. This is an abridged version as handed out at the first lecture.
-
Modelling and Analysis of Communicating Systems,
J.F. Groote and M.A. Reniers. 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.
A note on verifying your design by Mohammad Mousavi
Mohammad Mousavi wrote
a small note on how to verify requirements.
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.
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