7A Unit

Lecturers: Ali Abdallah and Jonathan Bowen

URL: http://www.cs.reading.ac.uk/cs/people/jpb/teaching/afm.html

See timetable and assessment information.

This optional 3rd year unit is based on research by the RUCS Formal Methods Group, part of the Formal Methods and Software Engineering Group. In the Autumn Term, Ali Abdallah will present formal methods for concurrent systems. In the Spring Term, Jonathan Bowen will introduce issues concerning the industrial use of formal methods, especially using the Z notation. A range of applications may be found in the book Applications of Formal Methods. The use of Z tools to type-check and animate Z specifications, and logic programming to rapid-prototype formally specified software and hardware systems will be explored, using case studies. The Z/EVES proof tool may also be introduced, depening on the interests of students taking this unit.

General information

Formal Methods and logic programming information, including Prolog, from the WWW Virtual Library.
Applications of Formal Methods book information and related publications for background reading.

Slides (in PostScript format):

Industrial Use of Formal Methods.

Note: please try to avoid printing the above to save paper. If you would like a printed copy of anything on-line that has not been handed to you by the lecturer in printed form, please ask the lecturer first.

Software tool support

The following software has been installed for the unit under /home/pub on the Sun network.

ZTC - a Z type-checker which accepts L^ATEX documents as input. Documentation includes a manual page (also in PostScript format), ztc.sty L^ATEX style file (which may be copies into your working directory and used in conjunction with zed-csp.sty style file (similar to zed.sty), and full PostScript documentation (issued in printed form). Run using ztc. A log file with extension .log is produced.
ZANS - a (prototype) Z animator. Run using zans. For information, see the printed tutorial. Remember ZANS is still under development and thus is not perfect.
L^ATEX - a document preparation system, whose input can be type-checked by ZTC. Run using latex. Input files have extension .tex; output files have extension .dvi. An auxilary file with extension .aux and a log file with extension .log are also produced (note possible clash with ZTC log output above). View the .dvi using xdvi and print it using dvips.
SWI-Prolog - a Prolog logic programming system. Run using pl. Help information is available within SWI-Prolog. For help, type "help(command)." at the ?- prompt (e.g., "help(help).") - remember the "." terminator followed by Carriage Return. To load a Prolog program from the file fred.pl, type "[fred]." (see Prolog example files *.pl under /home/pub/afm). To exit, type ^D (Control D - Unix end of file). See also on-line manual.
Z/EVES - a Z proof tool based on EVES. Run using z-eves. See also documentation and other files under /home/pub/z-eves/.

Getting started

The executable programs for these are available for Suns under /home/pub/bin and L^ATEX is under /packages/TeX/bin. . You should include these directories in your search path by editing your ~/.login file appropriately. E.g., towards the end of the file, include the following:

setenv PATH "${PATH}:/home/pub/bin:/packages/teTeX/bin/sparc-sunos4.1.3/"

Associated source files are under /home/pub/src, documentation in PostScript format under /home/pub/doc, and Unix manual pages are under /home/pub/man/man1. You can read these and manual pages associated with L^ATEX using the Unix man command by setting the manual page search path in your ~/.login file appropriately. E.g.:

setenv MANPATH "/usr/man:/usr/local/man:/usr/openwin/man" setenv MANPATH "${MANPATH}:/home/pub/man:/packages/teTeX/man"

If using a Computer Services Centre Sun workstation, you will need to rlogin to a Department of Computer Science Sun workstation to run latex with the zed-csp style file and associated special fonts successfully.

To use X windows-based programs on the remote workstation, include the following in your ~/.login file:

setenv DISPLAY "`who am i | sed -n 's/.*($[^:)]*$.*/\1/p'`:0"

Then xdvi may be used to view formatted L^ATEX output when run from the remote machine.

Files for use with this software will be placed under the directory /home/pub/afm as the unit progresses. An example Z specification is available as /home/pub/afm/pos-ztc.tex, together with other associated files.

To make and use a subdirectory called afm, copy the example files, LaTeX, view, type-check and produce PostScript formatted output suitable for eventual printing, use the following Unix commands:

cd mkdir afm cd afm cp /home/pub/ztc/ztc.sty /home/pub/afm/pos* . latex pos-ztc xdvi pos-ztc & ztc pos-ztc.tex dvips pos-ztc -o lpr -Plw pos-ztc.ps

Lines suitable for direct inclusion in your ~/.login file to help set up your environment correctly may be found in the file /home/pub/afm/login.

If you prefer to use PCs instead or as well, ZTC, ZANS and a version of Prolog are available under /home/pub/pc on the Sun network or under the P: drive in the PC laboratory for copying or direct use. You may use this software on your own PC if you wish. TrueType Z fonts for mathematical symbols are available on-line for PC Windows and Macs if you wish to use them with MS Word or other similar word processors.

Possible academic options for the future

Formal methods research at RUCS. It is possible to undertake formal methods research here, perhaps leading to a docorate.
M.Sc. in Computation at the Oxford University Computing Laboratory. This challenging course is recommended if you really like formal methods!
Courses on safety-critical systems.

Feel free to contact me for advice if you would like to consider any of the above options.