Requirement Analysis, Design and Verification (RADV, 2IW20)

Last update: February 19, 2004

Teachers: J.F. Groote and A.H.J. Mathijssen.

2nd trimester 2003/2004, monday 3/4 hour, HG 6.09 (during the full trimester), Thursday 1/2 hour, AUD 12 (during the first halve of the trimester). First lecture December 1, 2003. Intermediate exam January 22, 2004. Final date to hand in the report for the assigment March 26, 2004. Assignment and exam contribute evenly to the final score. The lecture notes are not allowed to be used at the exam.

Exercise 8.18

Aad Mathijssen wrote a small note on exercise 8.18 in which he gives in full detail how to show two processes equivalent using CL-RSP.

Note on Greibach Normal Form and prioritisation

Veena Parashuram made notes on Greibach Normal Forms and on priorisation that gewis kindly put on their website (removed).

Model exam

This model exam is indicative for the final exam that will take place on thursday, January 22.

Lemma 3.19

Aad Mathijssen found the proof of lemma 3.19 in the lecture notes too compact, and therefore, he wrote a fully detailed proof of it in .pdf format.

Literature:

Toolsets

The mcrl toolset can be used on the svstud.win.tue.nl (linux) for which all students can get an account at BCF (HG 8.73). Ask access to the directory /scratch/jfg2003 where large files can be stored. This can be done by BCF by putting you in an adequate group. All the programs reside in the directory /home/jfg/MCRL/bin. Example files are in /home/jfg/MCRL/data. In case of problems contact J.F.Groote@tue.nl. Most tools have a -help flag that gives a concise description of the tool and its use. All tools, except the simulator (msim) are command line driven. Many tools print their output to stdout, such that their results can be piped into other tools.

A Linux/MacOs/Unix version of this toolset can be obtained at the mcrl home page. This tool also runs on window machines under Cygwin (see mcrl/Cygwin executables). Installation of the toolset goes by following the instructions in the INSTALL file. In case of problems contact Bert Lisser (bertl@cwi.nl) with a clear and concise description of the problem.

The most important commands are mcrl, that checks the syntax and typing of a mcrl specification. With the flag -tbf, -regular or -regular2 a linear specification is generated into a compressed .tbf format. A known bug in mcrl is that it cannot deal with terminating processes. In case of non explainable crashes termination is often the problem.

The tool pp can be used to transform a .tbf file to readable text. The tool msim can simulate a specification. Instantiator can generate a statespace. Tools as constelm, parelm, structelm, invelm, confelm reachelm and others can be used to reduce the complexity of .tbf files.

It is also possible to use the Ceasar/Aldebaran toolset. This tool is also available on the svstud.win.tue.nl. In order to use the tool, the following commands must be executed when logging in:

setenv CADP ~jfg/CADP

setenv CADP_LANGUAGE english

setenv CADP_CC "gcc -I/usr/include"

setenv CADP_TMP /tmp

setenv CADP_PS_VIEWER ghostview

setenv EDITOR vi

setenv NAVIGATOR netscape

alias arch $CADP/com/arch

setenv FC2DIR ~jfg/FC2

Furthermore, the directories {$CADP}/com en {$CADP}/bin.`arch` must be added to the current search path. The home pagina of the Ceasar/Aldebaran toolset provides a lot of information, including the possibility to download the tool. For this a separate (free) license must be acquired, which is a hairy procedure, generally taking several weeks. A compiled and ready to run version of this toolset can be found in ~jfg/CADP/com.

Making pictures of transition systems

There are three ways to depict a transition system. The first way is with xeuca. For this a .aut file must be made using the instantiator. The .aut format is the default format of the instantiator. Using the flag -i an i is generated instead of a tau. The i is the standard for an internal action in the xeuca toolset.

The second way is by generating a .svc file, using the flag -svc in the instantiator. Using svc2dot, and subsequently dot -Tps file.dot > file.ps a picture in postscript format can be generated. The dot program can be found in the directory /home/jfg/bin.

The third way is by using the FSM visualizer of Frank van Ham. This gives by far the most spectacular results. This visualiser can be used by strating the program startfsm in the directory /home/jfg/bin. The program svc2fsm can be used to translate a svc file to a file readable for start fsm. If the -svc-term flag is used in the instantiator, svc2fsm file.svc file.tbf generates on stdout a .fsm file, from which in the tool values of variables can be inspected. The FSM visualiser is available for windows and linux machines and requires a decent graphics card. This program is also freely available. It can be found in the directories of Frank van Ham. Here also many visualised transition systems of various applications can be found.

Go back