Newsgroups: comp.parallel From: dmj@comlab.ox.ac.uk (David Jackson) Subject: Refinement Checking Tool for CSP Available Organization: Oxford University Computing Laboratory, UK Date: Tue, 16 Nov 1993 16:51:20 GMT Formal Systems (Europe) is pleased to announce the availaility of academic licences for its FDR refinement checking tool. The academic release is made possible by support from the US ONR. The distribution is available to educational institutions for a nominal media charge -- Formal Systems makes no profit from this release. The latest version (FDR 1.3) is now available. New features include X-windows interactive interface support Support for off-line and remote refinement checks Improved type-checker and parser More extensive debugging information Existing FDR users can obtain updates via FTP from the address given below, which can be used in conjunction with their existing LICENCE files. A N N O U N C I N G F D R ============================= FDR (standing for Failures Divergence Refinement) is a tool for proving properties of CSP programs. It is a product of Formal Systems (Europe) Ltd. It deals with a flexible syntax based on the CSP notation presented in Hoare's text. Support is also provided for handling the numbers, sets, sequences, etc, frequently used in processes' states and data-components of events. Developed for industrial applications, for example at Inmos where it is used to develop and verify communications hardware, it is now made available at nominal cost to academic institutions thanks to support from the US Office of Naval Research (ONR). FDR brings CSP to life for teaching, and provides an excellent tool for developing, debugging and finally proving programs written in it. It is supplied with a library of commented examples, including the dining philosophers, a train set, a voting system, and several communication protocols including the alternating bit and sliding window protocols. These examples are currently available by anonymous FTP, to enable potential users to see a sample of what FDR can do. A copy of the FDR manual, which contains a description of the syntax supported, can be obtained in the same way. Obtaining Information About FDR =============================== Information about the FDR system, including up-to-date versions of the manual, may be obtained via anonymous ftp from "ftp.comlab.ox.ac.uk", IP number "192.76.25.2". The files are stored in "/pub/Packages/FDR/public.info/" (See the end of this announcement for further details). Comments, suggestions, and questions about FDR should be addressed to "fdr-request@comlab.ox.ac.uk" Technical Details ================= The theory of refinement in CSP allows most correctness conditions (safety and liveness, but not fairness in the current version) to be encoded as the most nondeterministic process satisfying them. We can test whether an implementation meets the specification by deciding if it refines the specification process. FDR is therefore built around this decision question. It implements a normalisation procedure for the specification process, which represents the specification in a form where the implementation can be checked against it by model-checking techniques (exploring reachable states). Both the specification and the implementation must therefore be finite-state processes. The theoretical result that the normal form of a CSP process can be exponential in the number of states in the input has never proved problematic except in deliberately created pathological examples. In the majority of cases, checking is linear in the number of states in the operational semantics of the implementation. The system is currently built as a Standard ML program, which calls routines in C to perform the normalisation and model-checking functions. * * * * * * * * * * * * * The size of problem it can deal with depends on the amount of memory (both physical and swap) available on the machine you are using. It is able to make effective use of virtual memory in the model checking phase, making the number of states dealt with proportional to this. A few timings are given below based on a Sparc2 with 32Mb of physical memory and approximately 75Mb of swap space. They are all based on the example files, as indicated. File Spec Imp States Setup Check1(e/cpu) Check2Quick phils DF BSYSTEM 5151 35 30/20 9/7 trains RLIVE RSYSTEM 4260 25 20/14 7/4 swp1 SPEC SYSTEM 20480 230 121/113 12/11 swp2 OSPEC DC 117888 300 21m35s/21m8s 210/204 swp2 SPEC SYSTEM 919680 300 **** 29m/28m11s "File" is the example file from which the problem is taken. "Spec" and "Imp" are the processes from those files checked. "States" is the number of states visited in the model-checking phase. "Setup" is the approximate elapsed time taken by the SML front end to convert the already-parsed CSP programs into the compiled form used by the refinement checking programs. This time depends on the sum of the number of states in the low-level component processes that make up the specification and implemententation, and also the complexity of their definitions. If multiple use is made of definitions during a session, the caching of FDR allows much of this time to be saved for checks after the first. "Check1" gives the elapsed time for the rest of the refinement process, and cpu time for the model-checking phase, using one version of the refinement checker -- one which performs an explicit divergence check. "Check2Quick" gives the corresponding times for a version of the checker that does not test for divergence in the implementation, and therefore assumes absence of divergence. All times given are in seconds except where indicated. It can be seen that, for small problems, the setup phase tends to dominate the processing time, whereas for problems with large numbers of states it is the model-checking phase. * * * * * * * * * * * * * A subsequent version of the system will support various techniques for avoiding the explicit exploration of state spaces (which typically grow exponentially with the number of processes in a parallel system). This will allow, for example, the deadlock analysis of N dining philosophers in time linear in N, rather than the current exponential time. * * * * * * * * * * * * * Distribution and Support ======================== The software currently runs only on SUN Sparc systems (and clones), though alternative platforms are being investigated. 16Mb of physical memory is required by the system, and its performance will improve with more. Systems running FDR should have at least 60 Mb of virtual memory; those wishing to use it on large problems more. Formal Systems is planning to support other hardware (including PC-type systems) and various operating systems. Possible platforms include: Intel 3/486 based systems running OS/2, Linux, or BSD386 Apple Macintosh A/UX or Mach Ten systems IBM RS6000 AIX systems If you are interested in these or any other developments, please contact Formal Systems at the address below. The system is available to bona fide educational institutions for education and research use (i.e., non-profit) only for the nominal price detailed below. Formal Systems reserves the right to refuse this offer to any party at its absolute discretion. If you are unsure whether your institution will qualify for this offer, please write or FAX as indicated below with details. The system may be used by an unlimited number of users from a single installation at one site. A licence file is supplied which may not be copied except for backup, and which must be present for the software to run. This enables us to support the system by FTP: users will be supplied with details of how to receive updated versions of FDR. For the time being this service is supported by the ONR and free to users under this academic release. The software is supplied on 2 SUN `bar' format 3.5in disks, with a further disk containing the licence. An alternative to using the `bar' disks is to load the system less licence via FTP, and then install using only the licence disk. The software is available on DC6150 Tapes at additional cost. One copy of the manual, which may be copied, is supplied with the distribution, as are installation instructions. * * * * * * * * To obtain your copy of the system, please print out the following form, fill it in and post with cheque to Formal Systems (ref FDR) 3 Alfred Street Oxford OX1 4EH UK Enquiries from individuals or bodies who do not qualify under the terms of this offer are welcome. Please write to the above address, send a FAX to [+44] (0)865 201114, or telephone [+44] (0)865 728460 and ask for Dave Jackson or Michael Goldsmith. --------8<------------8<------------8<------------8<------------8<-------- FDR Academic Licence: Application form ====================================== Name of Institution: Site where software to be used: (above information will appear in licence) Address for delivery: Contact name/email address: Distribution required: Standard (bar disks): 200 pounds [ ] or 400 US dollars [ ] DC6150 Tape : 250 pounds [ ] or 500 US dollars [ ] VAT: Customers in the UK should add VAT at the prevailing rate. A VAT invoice will be sent with the software. Customers who are (i) within the European Community but outside the UK and (ii) are ordering subsequent to 1 December 1992 should either add VAT at the UK rate (17.5%) or provide their VAT number. The former will apply to customers who are not VAT registered, and customers who are VAT registered should normally do the second. This is necessary because of the VAT regulations connected with the Single European Market. Cheque or International Money Order should be sent with order. The price includes postage, but any customs or other dues payable will be the responsibility of the purchaser. --------8<------------8<------------8<------------8<------------8<-------- The above prices apply to academic institutions only, and use of the software is limited to education and non-commercial research. The licence issued will be non-transferrable. Obtaining Information via Anonymous FTP ======================================= Having called "ftp", you should proceed as follows: ftp> open ftp.comlab.ox.ac.uk 220-ftp.comlab.ox.ac.uk FTP server (Version 4.696 Tue Jun 9) ready. 220 Anonymous retrieval login with userid: `anonymous'; Name (ftp.comlab.ox.ac.uk:user): enter "anonymous" 331 Guest login ok, give your email address for password. Password: enter your email address: e.g. "user@comlab.ox.ac.uk". 230-Guest `user@comlab.ox.ac.uk' login ok, access restrictions apply. 230-Local time is now Fri Oct 23 18:00:36 1992 230-We have special access features, see file /README 230 It was last updated Tue Sep 15 09:24:58 1992 - 38.4 days ago ftp> enter "bin" (in case you're picking up any binary files: e.g., *.dvi) 200 Type set to I. ftp> enter "cd /pub/Packages/FDR/public.info/manual" 250 CWD command successful. ftp> enter "mget *" and type "y" to receive each file mget manual.ps? y 200 PORT command successful. 150 Opening BINARY mode data connection for /pub/Packages/FDR/public.info/manual /manual.ps (492098 bytes). 226 Transfer complete. local: manual.ps remote: manual.ps 492098 bytes received in 3.6 seconds (1.3e+02 Kbytes/s) ftp> to get example files, you should then enter "cd /pub/Packages/FDR/public.info/examples" ftp> 250 CWD command successful. ftp> enter "mget *" mget 00.examples? y 200 PORT command successful. 150 Opening BINARY mode data connection for /pub/Packages/FDR/public.info/examples/00.examples (3229 bytes). 226 Transfer complete. local: 00.examples remote: 00.examples 3229 bytes received in 0.37 seconds (8.6 Kbytes/s) mget abp.csp? y 200 PORT command successful. ... etc. ftp> quit Problems with FTP? ================== Note that if the server fails to recognise your address, the following message will be displayed: 230-Guest `no_such_user@mars' login ok, access restrictions apply. 230-Hmm.. You didn't give your complete email address for password, - Please, next time give your Internet email address. - Example: Example.Name@pierrot.comlab.ox.ac.uk 230-Local time is now Fri Oct 23 18:19:54 1992 -Your IP number didn't reverse, and/or password wasn't ok as email address. -Read /CAPTIVE-README for further information! 230-We have special access features, see file /README 230 It was last updated Tue Sep 15 09:24:58 1992 - 38.4 days ago and you will unable to retrieve files. Should this occur, close the connection by typing "close" and try again. ============================================================================ E-mail facilities of the University of Oxford used by their courtesy. Trademarks are acknowledged as the property of their respective owners. -- David M. Jackson - Research Student - Oxford Univ. Programming Research Group David.Jackson@prg.ox.ac.uk 11 Keble Rd, Oxford, UK. Tel.+44-865-273846