🚀 go-pugleaf

   This is a reposting of the announcement that Formal Systems, Ltd. will be
offering short courses on Z and on CSP at Tulane University this April.  There
are three new points to note:
   (1) A reduced rate is available for those who participate in both courses.
       Also, an academic rate has now been established for the courses.
   (2) We are asking that those who intend to take either of the courses
       pre-register by March 1.
   (3) Our apologies for the inconvenience, but news etiquette prevents our
       posting the course fees.  Anyone wanting this information should send
       email to: mwm@tulmath.math.tulane.edu

A description of both courses follows.

===========================================================================

                    Formal Systems (Europe), Ltd

                        Course Announcement I:  

                     Formal Development Using Z
                       A Tool-Based Course


                        April 5 - 9, 1993 
                        Tulane University
                    New Orleans, Louisiana USA


                        Course Lecturer:  
                        J.C.P. Woodcock


Formal Systems (Europe) Ltd exploits pioneering work in the field of
Formal Methods. The directors and staff include key current and former
members of the Programming Research Group at Oxford University,
England, each with an established international reputation. The company
has extensive industrial experience of the pragmatic application of
formal techniques to the analysis and design of both software and
hardware systems, in Europe and the USA.

Since its formation in 1989, Formal Systems has doubled in staff and in
turnover each year. Past and present clients for consultancy include
Inmos Ltd on VLSI design quality assurance, Deutsche System Technik on
formal specification, C.S. Draper Laboratory on fault-tolerant
processors, and Secure Information Systems Ltd on formal verification.
Additionally, Formal Systems is a collaborator in European Community
ESPRIT activities and has given specialized industrial short courses in
conjunction with Oxford University in the UK and Tulane University in
the USA. In 1991 Formal Systems received a prestigious SMART Award from
the UK Department of Trade and Industry for technological innovation in
an aerospace engineering application.

Z is a specification language based on mathematical set theory and
logic. It was developed at Oxford University for use in the
specification of state-based programs, and has now matured into a
valuable and widely used development tool.  For example, IBM UK
Laboratories at Hursley have used  Z  to develop approximately 48,000
lines of new code for the CICS system (the main IBM System/370 on-line
transaction processing system).  They obtained a significant reduction
in the volume of software quality defects for ultimately little
additional development cost.  For this achievement, IBM UK Laboratories
and Oxford University Computing Laboratory (PRG) were jointly presented
with a prestigious Queen's Award for Technological Achievement in
1992.  Z has proved itself to be especially useful as a tool for
formally verifying and demonstrating the correctness of safety critical
and/or secure systems.

Objectives:  We present the Z notation, together with systematic
techniques for developing designs and code from Z specifications.
Mechanical assistance in managing specification and proof will be
demonstrated using a mechanical proof assistant .

An understanding of elementary logic and set theory is useful.

                        Program
 
Lectures and tutorials will cover the following topics:

- Logic. Sets, relations and functions, sequences. Mathematical toolkit.

- Schemas and schema operations. Using schemas to structure specifications.

- Data refinement. Operation refinement. Program development.

- Methods of proof. The mechanization of proofs.

- Case studies, workshop exercises.

- The role of formal methods in software development.

Dr J. C. P. Woodcock is Director of External Studies at Oxford
University Computing Laboratory, as well as being a Director of Formal
Systems. His research interests include specification, refinement and
proof of sequential and concurrent systems, security, and technology
transfer.  He has been a consultant for IBM for the last six years
working on formally specifying and analyzing the CICS system.  As a
consultant to IBM for six years, he was a key member of the team who
won the Queen's Award (see above) for specifying and analyzing the CICS
system.  He has taught courses in formal methods to over 1500 students
from industry and academia.

Location        Tulane University
		New Orleans, LA

Date            April  5 - 9,  1993

Duration        Four and a half days
		(ends lunchtime Friday)

Course Fee      $xxxx per person includes course materials, lunches and 
                a course dinner.  Inquire for block rates.

Accommodation   Hotel accommodation is available for $xx/night plus tax.       
                Alternatively, a list of hotels can be supplied on request.

Contact         Professor Michael Mislove
		Department of Mathematics 
                Tulane University 
                New Orleans, LA  70118 
                (504) 865-5727
	        (mwm@tulmath.math.tulane.edu)


                          Booking Form

                   Formal Development Using Z 
                       April  5-9,  1993


Number of participants : ______

Name

____________________________________________________________________


____________________________________________________________________

Accommodation Required (Give Dates)

____________________________________________________________________


____________________________________________________________________

Contact address:

____________________________________________________________________


____________________________________________________________________


Phone:________________________

Bookings should be made as soon as possible.

Course fee: A deposit of $xxx is required with order (deadline: March 1, 1993).  
            Balance is due by March 31, 1993.

Formal Systems (Europe) Ltd. and Tulane University reserve the right to
cancel the course prior to March 31st if it is undersubscribed.

===============================================================================


                   Formal Systems (Europe), Ltd


                      Course Announcement II:

                       Introductory CSP
                      A Tool-Based Course


                     April 12 - 16, 1993
                      Tulane University
                    New Orleans, Louisiana


          Course Lecturers: A.W. Roscoe and G.M. Reed


Formal Systems (Europe) Ltd. exploits pioneering work in the field of
Formal Methods. The directors and staff include key current and former
members of the Programming Research Group at Oxford University,
England, each with an established international reputation. The company
has extensive industrial experience of the pragmatic application of
formal techniques to the analysis and design of both software and
hardware systems, in Europe and the USA.

Since its formation in 1989, Formal Systems has doubled in staff and in
gross income each year. Past and present clients for consultancy
include Inmos Ltd on VLSI design quality assurance, Deutsche System
Technik on formal specification, C.S. Draper Laboratory on
fault-tolerant processors, and Secure Information Systems Ltd on formal
verification.  Additionally, Formal Systems is a collaborator in
European Community ESPRIT activities and has given specialized
industrial short courses in conjunction with Oxford University in the
UK and Tulane University in the USA. In 1991 Formal Systems received a
prestigious SMART Award from the UK Department of Trade and Industry
for technological innovation in an aerospace engineering application.

Communicating Sequential Processes (CSP) is a notation for the
specification, design, and analysis of concurrent and distributed
systems.  The theory and application of CSP as an analytical tool has
been developed over the past fifteen years by European academics and
industry.  Furthermore, CSP has been implemented in the form of occam*
and the Transputer.  It is particularly suited for the verification of
expressive power of CSP allows the representation of most of the usual
descriptions of finite state systems,  such as the state transition
systems, Petri nets, many classes of automation, and -- in some
applications -- languages such as VHDL.

The course introduces all the important ideas of CSP, and will bring
participants to the point where they can understand what CSP is and
where it is applicable,  and have the ability to apply it to problems
in their own domain.

It is centered around a newly developed software tool (FDR), a product
of Formal Systems. FDR tests for Failures- Divergence Refinement, a
powerful and flexible method based on the standard model of CSP.  This
permits verification of both simple and complex specifications of
systems and also direct comparison of different implementations.  Where
a property fails to hold,  FDR has powerful debugging capabilities to
isolate faulty components.  FDR was originally developed as a result of
collaborative work between Formal Systems and Inmos Ltd as a tool for
verifying VLSI designs.  It is now a general purpose tool for the
design and verification of software and hardware systems.

By using FDR, students on the course will see CSP come to life, and
learn to use a tool with the capability of dealing with realistically
sized problems.

___________________________ 
 *occam is a trademark of INMOS Ltd


                         Program  

Lectures and  tutorials will cover the following topics:

- Interfaces 	- Case Studies 		- Safety Properties     
- CSP Laws 	- Non-determinism   	- Deadlock 
- Refinement	- Timed CSP 		- Liveness Properties   
- Comparison with other notations

Dr A. W. Roscoe and Dr G. M. Reed are both Directors of Formal Systems
and Senior Faculty in Computation at Oxford University.  Both are
pre-eminent researchers in CSP.  Dr Roscoe was one of the original
developers of the language and its theory.  He is an authority on
deadlock avoidance techniques, and he is the chief designer of FDR.
Dr  Reed is best known for his work on Timed CSP, and now leads a large
group at the University developing methods for using CSP in industry.

Dr Roscoe is a University Lecturer at Oxford University and a Fellow of
University College, specializing in the theory of parallel computing
and its applications. He is a co-inventor of the failures model for
CSP, the developer of the standard semantics for  occam, and the
director of the team which produced the occam Transformation System
used in the design of the floating-point Transputer.  He is also a
leading authority on the analysis of deadlock in parallel networks.

Dr Reed is a University Lecturer in Computation at Oxford University
and a Fellow of St Edmund Hall. He and Dr Roscoe have developed the
theory of real- time distributed computing based on CSP.  There is
currently a large group at Oxford under his direction devoted to making
this theory of practical use for industrial application.


Location        Tulane University
		New Orleans, LA

Date            April 12-16, 1993

Duration        Four and a half days
		(ends lunchtime Friday)

Course Fee      $xxxx per person Includes course materials, lunches and 
                a course dinner.  Inquire for block rates.


Accommodation   Hotel accommodation is available for $xx/night plus tax.  
		Alternatively, a list of hotels can be supplied on request.


Contact 	Professor Michael Mislove
		Department of Mathematics 
		Tulane University 
		New Orleans, LA  70118 
		(504) 865-5727
		(mwm@tulmath.math.tulane.edu)


                         Booking Form

                      Introductory CSP 
                     April 12-16, 1993


Number of participants : ______

Name

____________________________________________________________________


____________________________________________________________________

Accommodation Required (Give Dates)

____________________________________________________________________


____________________________________________________________________

Contact address:

____________________________________________________________________


____________________________________________________________________


Phone:________________________

Bookings should be made as soon as possible.

Course fee: A deposit of $xxx is required with order (deadline March 1).  
            Balance is due by March 31, 1993.

Formal Systems (Europe) Ltd. and Tulane University reserve the right to
cancel the course prior to March 31st if it is undersubscribed.