[Prev][Next][Index]
FME'96
University of Oxford
FORMAL METHODS EUROPE
FME'96
Tutorials and International Symposium
18--22 March 1996
Call for Participation
Programme
Sponsored by the Commission of the European Communities
CRI
Formal Systems (Europe) Ltd
IFAD
Oxford University
Praxis plc
Prentice Hall International
FORMAL METHODS EUROPE
FME'96
Tutorials and International Symposium
18--22 March 1996
FME'96 will be held at St Hugh's College, Oxford University, England,
from Monday 18th to Friday 22nd March 1996. The Tutorials will take
place on Monday 18th and Tuesday 19th March, and the Symposium will
take place on Wednesday 20th--Friday 22nd March, inclusively.
The event is organised by Formal Methods Europe, the advisory panel of
the Commission of the European Communities. Local arrangments are
being made by the Oxford University Centre for Continuing Professional
Development.
SYMPOSIUM SPONSORS
The Symposium is sponsored by the Commission of the European
Communities, CRI, Formal Systems (Europe) Ltd, IFAD, Oxford
University, Praxis plc, and Prentice Hall International.
CONFERENCE VENUE
The Tutorials and Symposium will be held at St Hugh's; this includes
all lectures, poster sessions, and tool demonstrations. Accommodation
is also available at St Hugh's, as well as at Lady Margaret Hall and
at Rewley House, both of which are just a short walk from St Hugh's.
St Hugh's College in the University of Oxford is situated in 14 acres
of parkland, less than a mile from the centre of Oxford, one of the
most beautiful cities in Europe. The College was founded in 1886 by
Elizabeth Wordsworth, great-niece of the poet William Wordsworth. She
named the College after St Hugh, the mediaeval Bishop of Lincoln,
because her father was himself Bishop of Lincoln, and his legacy was
used to found the College. For a century St Hugh's remained a women's
college, but in 1986 the College Charter was changed to admit men; the
College now has almost five hundred mixed students.
SYMPOSIUM BANQUET
On Thursday 21st March, there will be a Drinks Reception followed by a
Symposium Banquet in the Dining Hall at St Hugh's College.
COLLEGE ACCOMMODATION
College accommodation will be provided throughout the Tutorials and
Symposium at St Hugh's College, Lady Margaret Hall, and Rewley House.
There is a choice of rooms with en suite bathroom, or with shared
facilities; there are single and double rooms. The accommodation is
comfortable, if unpretentious. En suite accommodation with breakfast
costs 45 pounds sterling per person, per night; with shared
facilities, the cost is 35 pounds sterling per person, per night.
HOTEL ACCOMMODATION
Arrangements can be made for those who prefer to stay in a hotel.
Please contact Anna Morris on +44 (0)1865 288169.
TRAVEL
Oxford has excellent rail and road links, with frequent bus and train
services to and from London and all other major cities in the UK.
There are direct coach services to Heathrow and Gatwick Airports. The
journey from Heathrow Airport to the centre of Oxford takes just 90
moniutes. Travel details will be sent to all delegates with their
Registration Information, before the start of the event.
TUTORIAL PROGRAMME
There are eight Tutorials, each lasting a half-day. They are
organised in two parallel tracks during Monday 18th and Tuesday 19th
March.
Monday 18th March
Track 1 morning:
Formal Development of Object-Oriented Systems in VDM++
S. Goldsack & K. Lano, Imperial College, London
The tutorial is aimed at users of formal methods such as Z and VDM who
wish to extend the use of formal techniques to concurrent and
real-time systems, and to include object-oriented structuring
facilities. It is also aimed at users of object-oriented techniques
who wish to introduce more rigorous methods into the specification and
design of object-oriented systems. No knowledge of VDM++ will be
assumed, although knowledge of object-oriented techniques and
terminology would be useful.
Track 1 afternoon:
RSML and its Application to TCAS II (Traffic alert and Collision
Avoidance System II)
Mats Heimdahl, Michigan State University
This tutorial describes an approach based on hierarchical finite state
machines (RSML - Requirements State Machine Language) that has been
successfully used to develop the software requirements specification
for a large commercial avionics system (TCAS II - Traffic alert and
Collision Avoidance System II). During this project, the RSML
notation was found to be easy to use and gained wide acceptance in the
joint industry government committee developing the requirements. We
will present the syntax and formal semantics of the RSML notation and
cover guidelines for how it should be used when specifying a complex
system. The language and guidelines will be illustrated with examples
and experiences from the TCAS II requirements specification effort.
The tutorial will also cover automated analysis techniques applicable
in the RSML framework and give examples of some of the problems these
techniques found in the TCAS II specification.
Track 2 morning:
CSP and FDR
Bill Roscoe, Formal Systems (Europe)Ltd
The combination of CSP and FDR has proved itself over the past few
years in a wide variety of practical and industrial applications.
This tutorial provides an introduction to the main ideas of CSP and a
description of how a variety of applications can be modelled in it and
analysed using FDR. Topics covered will include:
* The concept of communication and CSP model of handshake
synchronisation
* The main operators of CSP
* Specification using traces and refusal sets
* The concepts and basic use of FDR
* Case-study: communications protocol development
* Survey of how CSP/FDR have been applied to other areas
* Brief description of the advanced features of FDR 2
The tutorial will include live demonstrations of FDR
Track 2 afternoon:
An Introduction to Some Advanced Capabilities of PVS
Sam Owre & John Rushby, SRI International
This tutorial will review briefly the basic capabilities of PVS and
then move on to several of its more advanced capabilities and recent
extensions. The purpose of the tutorial is to give attendees an
appreciation for the scope and power of modern mechanizations of
formal methods, and for the opportunities these create for efficient
and effective use of formal methods in a variety of application areas.
Familiarity with PVS is not required, but current users of the system
should find the material directly applicable in their own work. The
tutorial will be conducted as a live demonstration using a workstation
with projection capabilities.
Tuesday 19th March
Track 1 morning:
Formal Development in B Abstract Machine Notation
K. Lano & H. Haughton, Imperial College and J.P. Morgan Ltd
The tutorial will give a comprehensive introduction to B Abstract
Machine Notation (AMN), a formal method which has been used in
substantial industrial software development in Europe, particularly
within IBM and for the French Railways. We will describe the
background of the language, its connection with the Z specification
language, and incrementally introduce the notation and method through
a variety of examples. The language and method covers all software
life-cycle stages from requirements through to code generation and
maintenance, although specification and design will be the main topic
of the tutorial.
Track 1 afternoon:
Action Semantics
Peter Mosses, University of Aarhus
Action Semantics is useful for specifying programming languages:
documenting design decisions, setting standards for implementation,
etc. This framework has unusually good pragmatics, making
specifications easily accessible to programmers. Thanks to its
inherent modularity, action semantics scales up smoothly to describing
practical, industrially useful languages. In this tutorial, action
semantics is explained, illustrated, and compared to other frameworks
such as VDM and RAISE.
Track 2 morning:
ACL2
Matt Kaufmann, J Strother Moore, and William D. Young, Computational
Logic Inc.
ACL2 is an extended, reimplemented version of Nqthm that supports the
applicative subset of Common Lisp as its logic. We discuss the logic,
the theorem prover, certain system engineering features, and examples.
By formalizing a logic around applicative Common Lisp we can take
advantage of the exceptionally good optimizing compilers for Common
Lisp to get, in many cases, execution speeds comparable to C. Two
guiding tenets of the ACL2 project has been to conform to all
compliant Common Lisp implementations and to add nothing to the logic
that violates the understanding that the user's input can be submitted
directly to a Common Lisp compiler and then executed in an environment
where suitable ACL2-specific macros functions are defined.
Track 2 afternoon:
The ProCoS Approach to the Design of Real-time Systems: linking
different formalisms
Anders Ravn, DTU
The proposed tutorial focuses on the need to link the different
formalisms that are used in a development path from specification of
requirements to executable programs or specialized hardware. General
linking paradigms for compiler verification, transformation from
specifications to programs, and transformation from state to event
based formalisms are illustrated with examples taken from the
real-time formalisms developed in the Provably Correct Systems
(ProCoS) project.
CONFERENCE PROGRAMME
Wednesday March 20
09.00--10.00 INVITED LECTURE
- How Did Software Get So Reliable Without Proof?
C A R Hoare, Oxford University, UK
10.30-11.30 Session 1: B
- Quantitative Analysis of an Application of Formal Methods
Bicarregui Juan, Dick Jeremy, and Woods Eoin, Rutherford Appleton
Laboratory, B-Core, Sybase, UK
- Applying the B Technologies to CICS
Hoare J., Dick J., Neilson D., and Sorensen I., IBM and B-CORE, UK
11.30-12.30 Session 2 : Action Systems
- Refining Action Systems within B-Tool
Walden M. and Sere K., Abo Akademi Univ. and Univ. Kuopio, Finland
- Integrating Action Systems and Z in a Medical System Specification
Kasurinen V. and Sere K., Univ. Kuopio, Finland
14.00--15.30 Session 3a: Requirements
- Formalizing Anaesthesia - a Case Study in Formal Specification
Groenboom R., Saaman E., Rotterdam E., and Renardel de Lavalette G.,
Univ. Groningen and Univ. Hospital Groningen, NL
- A New System Engineering Methodology Coupling Formal Specification
and Performance Evaluation
Martins J. and Hubaux J.-P., EPFL, CH
- Formalizing New Navigation Requirements for NASA's Space Shuttle
Di Vito Ben, ViGYAN, Inc., USA
14.00--15.30 Session 3b: VDM
- Combining VDM-SL Specifications with C++ Code
Frohlich B. and Larsen P.G., IFAD, DK
- Data Reification without Explicit Abstraction Functions
Clement T., Univ. Manchester, UK
- Formal and Informal Specifications of a Secure System Component:
Final Results in a Comparative Study
Brookes T. M. , Fitzgerald J. S., and Larsen P.G., British Aerospace,
CSR-Newcastle, UK, and IFAD, DK
16.00--17.30 Session 4a: User Interfaces for Formal Methods
- Visual Verification of Safety and Liveness
Valmari A. and Setala M., Univ. Tampere, FIN
- Graphical Development of Consistent System Specifications
Broy M., Hussmann H., and Schaetz B., Univ. Munchen and Siemens AG, D
- Deduction in the Verification Support Environment (VSE)
Hutter D., Langenstein B., Sengler C., Siekmann J.H., Stephan W.
and Wolpers A., DFKI,Saarbrucken, D
16.00--17.30 Session 4b: Z
- Consistency and Refinement for Partial Specification in Z
Boiten E., Derrick J., Bowman H., and Steen M., University of Kent, UK
- Combining Statecharts and Z for the Design of Safety-Critical
Control Systems
Weber M.,Tech. Univ. Berlin, D
- Integrating Real-time Scheduling Theory and Program Refinement
Fidge C.J., Utting M., Kearney P., and Hayes I.J., Univ. Queensland,
Australia
Thursday March 21
09.00--10.00 Invited Lecture
- A Case Study on the Formal Development of a Reactor Safety System
Terje Sivertsen, OECD Halden Reactor Project, NO
10.30-11.30 Session 5: Distributed Systems (1)
- Using a Logical and Categorical Approach for the Validation
of Fault-Tolerant Systems
Seguin C. and Wiels V., CERT-ONERA, Toulouse, F
- Local Nondeterminism in Asynchronously Communicating Processes
De Boer F.S. and van Hulst M., Utrecht Univ.,NL
11.30-12.30 Session 6: Larch and LP
- Identification of and Solutions to Shortcomings of LCL, a LARCH/C
interface Specification Language
Chalin P., Grogono P., and Radhakrishnan T., Univ. Concordia, Quebec
- Formal Specification and Verification of the pGVT Algorithm
Kannikeswaran B., Radhakrishnan R., Frey P. Alexander P., and WIlsey
P.A. Univ. Cincinnati, USA
14.00--15.30 Session 7a: Model Checking (1)
- Automatic Verification of a Hydroelectric Power Plant
Pugliese R. and Tronci E., Univ. di Roma and Univ. di L'Aquila, I
- Experiences in Embedded Scheduling
Jackson David M., Formal Systems (Europe) Limited, UK
- Model Checking in Practice; An Analysis of the ACCESS.bus Protocol
using SPIN
Boigelot B. and Godefroid P., Univ. de Liege, B, and AT&T-Bell
Laboratories, USA
14.00--15.30 Session 7b: Distributed Systems (2)
- The Incremental Development of Correct Specifications for
Distributed Systems
Kleuker S. and Tjabben H., Univ. Oldenburg and Philips Research Lab.,
D
- A Theory of Distributing Train Rescheduling
George Chris, UNU/IIST, Macau
- An Improved Translation of SA/RT Specification Model to High-Level
Timed Petri Nets
Shi L. and Nixon P., Manchester Metropolitan University, UK, and
Trinity College, IR
16.00--17.00 Session 8: Testing and Debugging
- From Testing Theory to Test Driver Implementation
Peleska J. and Siegel M.,JP Sofware Consulting and Univ. Kiel, D
- Program Slicing using Weakest Preconditions
Comuzzi J.J. and Hart J.M., PERITUS Software Systems, USA
Friday March 22
09.00--10.00 Invited Lecture
Test Automation for Safety-Critical Systems: Industrial Application
and Future Developments
Jan Peleska, JP Software-Consulting and University of Bremen
10.30-11.30 Session 9: Architecture and Reuse
- A Formal Approach to Architectural Design Patterns
Alencar P. S. C., Cowan D. D., and Lucena C. J. P., University of
Waterloo, CA, and PUC, Brazil
- Modular Completeness: Integrating the Reuse of Specified Software
in Top-Down Program Development
Zwiers J., Hannemann U., Lakhneche Y., Roever W.P., and Stomp F.
Univ. Twente, NL, Univ. Kiel, D, AT&T Bell Lab., USA
11.30-12.30 Session10: Transformations
- A Strategic Approach to Transformational Design
Bohn J. and Janssen W., Univ. Oldenburg, D
- Correct and User-Friendly Implementations of Transformation Systems
Kolyang, Santen T. and Wolff B., Univ Bremen and GMD, D
14.00--15.30 Session 11: Model Checking (2)
- An Example of use of Formal Methods to Debug an Embedded Software
Arnold A., Begay D., and Radoux J.-P., Univ. Bordeaux and
SERLI-informatique, F
- Experiments in Theorem Proving and Model Checking for Protocol
Verification
Havelund K. and Shankar N., LITP Paris,F, SRI, USA
- Procedure-Level Verification of Real-time Concurrent Systems
Farn W. and Chia-Tien L., Academia Sinica, Taiwan
REGISTRATION
Registration for the Tutorials will take place at St Hugh's College on
Sunday 17th March 1996, between 14.00 and 1800. A Welcome Reception
will also be held between 18.30 and 19.00 at St Hugh's. Delegates
arriving on Monday morning can register between 08.00 and 09.00.
Registration for the Symposium will take place at St Hugh's College on
Tuesday 19th March between 14.00 and 18.00. A Welcome Reception will
also be held between 18.30 and 19.00 at St Hugh's. Delegates arriving
on Wednesday morning can register between 08.00 and 09.00.
The Tutorial Registration Fee for delegates registering before 19th
February is 225 pounds sterling. This covers the Welcome Reception on
Sunday 17th March, tutorial papers, attendance at all the tutorial
sessions, and the lunches and the daytime refreshments on 18th and
19th March. For delegates booking after 19th February, the Tutorial
Registration Fee is 235 pounds sterling.
The Symposium Registration Fee for delegates registering before 19th
February is 315 pounds sterling. This covers the Welcome Reception on
Tuesday 19th March, the Symposium Proceedings, attendance at all the
Symposium sessions, the lunches and the daytime refreshments on 20th,
21st, and 22nd March, and the Drinks Reception and Banquet on Thursday
21st March. For delegates booking after 19th February, the Symposium
Registration Fee is 330 pounds sterling.
The Combined Tutorial and Symposium Registration Fee which entitles a
delegate to all the above, for delegates registering before 19th
February is 475 pounds sterling. For delegates booking after 19th
February, the Combined Tutorial and Symposium Registration Fee is 500
pounds sterling.
Bookings should be made on the enclosed registration form, and
returned as soon as possible to Anna Morris, CPD Centre, Oxford
University, 1 Wellington Square, Oxford OX1 2JA, England. Please make
cheques payable to OUDCE. Payment must be made in pounds sterling.
delegates paying with cheques drawn on non-UK banks or by credit card
(VISA or MASTERCARD only), should add an additional 15 pounds sterling
to cover bank charges. Please telephone or fax to request a special
form for payment by credit card. We cannot confirm your registration
without payment, and we reserve the right to refuse admission if
payment has not been made.
Partners can be accommodated in double rooms. The Registration Fee
for Partners is 30 pounds sterling. This includes the Symposium
banquet and a reception.
CANCELLATIONS
Full refunds of registration and accommodation fees, less 25%
administration costs, are payable for cancellations received in
writing on or before 19th February. After this date, no fees are
refundable; howver, substitutions may be made at any time.
######################################################################
FORMAL METHODS EUROPE 1996 PLEASE indicate registration fee:
REGISTRATION FORM
Tutorial @ 225 pounds [ ]
(until 18.2.96)
please register the following @ 235 pounds [ ]
delegate for the symposium (after 18.2.96)
and/or tutorial sessions
Symposium @ 315 pounds [ ]
(for multiple registrations or (until 18.2.96)
partners please make copies of Symposium @ 330 pounds [ ]
this form) (after 18.2.96)
Tutorial and symposium @ 475 [ ]
Title (Dr/Mr/Ms) (until 18.2.96)
Tutorial and symposium @ 500 [ ]
______________________________ (after 18.2.96)
Partner registration @ 30 [ ]
First Name
Bank charge @ 15 pounds [ ]
______________________________ (credit cards or non-UK cheques)
IF you would like college
Family Name/Surname accommodation, please indicate
your choice of room:
______________________________
College accommodation [ ]
(single room, ensuite facilities)
Position/Job Title
College accommodation [ ]
______________________________ (single room, shared facilities)
College accommodation [ ]
Organisation (double room, ensuite facilities)
______________________________ College accommodation [ ]
(double room, shared facilities)
Full mailing address IF you are staying in college,
then bed and breakfast is
______________________________ available. Please indicate the
days on which this is required:
______________________________
Saturday 16th March [ ]
______________________________ Sunday 17th March [ ]
Monday 18th March [ ]
______________________________ Tuesday 19th March [ ]
Wednesday 20th March [ ]
Thursday 21st March [ ]
Postal code __________________ Friday 22nd March [ ]
Country ______________________ Total fee payable _______
Telephone ____________________ PLEASE indicate method of payment:
Fax __________________________ cheque enclosed [ ]
invoice required [ ]
Email ________________________ credit card form required [ ]
PLEASE RETURN THIS FORM TO: ANNA MORRIS, CPD CENTRE,
UNIVERSITY OF OXFORD, 67 ST GILES, OXFORD, OX1 3LU, UK
TELEPHONE +44 (1865) 288169 FAX +44 (1865) 288163