lm@lln-cs (Lynn Marshall) (07/12/88)
VDM-Europe Symposium '88
VDM: the way ahead
12-16 September 1988
Trinity College, Dublin, Ireland
organised by VDM-Europe
in cooperation with the Commission
of the European Communities
VDM is the acronym for the Vienna Development Method. VDM is applied
industrially and commercially in the systematic development of large
software systems by a growing number of European companies. The CEC
and several Community Member States are sponsoring a growing number
of projects which apply or develop various aspects of VDM.
The CEC has established a VDM-Europe Group which meets regularly to
discuss issues of VDM experience: use and applications, education and
training, tools, foundations, and standardisation.
After a successful first symposium in Brussels, in March 1987, VDM'88
will be an excellent opportunity to remain (or to become) informed on
the actual state-of-the-art of VDM, on experience in using VDM in real
industrial projects, on VDM tools and standards, and on the relation
between VDM and other formal software development methods.
The conference will be complemented by a two-day tutorial and an
exhibition. The tutorial, presented by Dines Bjoerner and Cliff Jones,
is a unique opportunity for anyone interested in an introduction to
VDM. The exhibition will enable symposium attendees to be updated on
VDM tools and VDM training. In addition to that, several VDM related
projects will present their results.
Programme Committee:
D. Bjoerner, Dansk Datamatik Center and Technical University of Denmark.
A. Blikle, Institute of Computer Science, Polish Academy of Sciences,
Poland.
R. Bloomfield, Adelard, UK.
T. Denvir, Praxis Systems, UK.
C. B. Jones, Department of Computer Science, University of Manchester, UK.
R. B. Jones (secretary), ICL, UK.
H.-J. Kugler, Generics Software Ltd., Ireland.
H. Langmaack, Institut fuer Informatik und Praktische Mathematik,
Christian-Albrechts-Universitaet zu Kiel, Germany.
L. S. Marshall (chairman), Unite d'Informatique, Universite Catholique de
Louvain, Belgium.
S. U. Palm, Dansk Datamatik Center, Denmark.
U. Schmidt, Norsk Data GmbH, Germany.
K. De Vriendt, Commission of the European Communities, Belgium.
Tutorial:
Presented by D. Bjoerner (Specification Principles) and C. B. Jones
(Development Principles).
Aims and Objectives: Survey the VDM landscape; familiarize participants
with the VDM terminology; encourage them to read VDM specifications and
developments.
Day 1: 12 September, 1988 (Monday)
Specification Principles (D. Bjoerner)
The first part of the tutorial will cover items such as: representational
and operational abstraction; applicative and imperative models;
denotational vs. computational semantics; abstract syntax; syntactic
and semantic domains; semantic functions; well-formedness and invariant
context; constraint conditions; putative and pre/post definitions.
Concepts introduced will be illustrated via applications in the areas of:
data bases, programming languages, and office systems.
The day will follow Dines Bjoerner's book "Software Architecture and
Programming Systems Design".
Day 2: 13 September, 1988 (Tuesday)
Development Principles (C. B. Jones)
This part of the VDM tutorial explains how to progress from a formal
specification. The design process is broken into steps whose correctness
can be verified. It is an essential part of this Development Method
that verification is possible before work on subsequent design/coding
takes place: this reduces the need for the scrap-and-rework which
drastically reduces the productivity of computer system development.
Formal specifications achieve brevity by the use of abstract objects for
the underlying model and by specifying operations by pre-/post-conditions.
The design steps are involved with finding concrete realizations for
both of these abstractions. The tutorial will describe both data
reification and operation decomposition.
The day will follow Cliff Jones's book "Systematic Software Development
using VDM". It will not be possible -- in one day -- to cover all of
the book, and the idea will be to convey the intuition behind this part
of VDM.
Conference Program:
Day 1: 14 September, 1988 (Wednesday)
0900-1030: Welcome; L. S. Marshall (Universite Catholique de Louvain,
Belgium)
Computing is a Physical Science; Invited speaker: Donald I. Good
(Computational Logic Inc., USA)
1100-1230: Structuring for the VDM Specification Language; Stephen Bear
(CEGB, UK)
Correctness for Beginners; Maurice Naftalin (University of
Stirling, UK)
1400-1530: Understanding an Informal Description: Office Documents
Architecture, an ISO Standard; Andrzej Borzyszkowski,
Stefan Sokolowski (Polish Academy of Sciences)
Towards a Formal Definition of GKS and Other Graphics
Standards; Clive Ruggles (University of Leicester, UK)
1600-1730: Report from the VDM Panel for the Standardisation of VDM
(IST/5/50); Derek Andrews (University of Leicester, UK)
Formal Methods in Standards -- A Report from the BCS Working
Group; Clive Ruggles (University of Leicester, UK)
Day 2: 15 September, 1988 (Thursday)
0900-1030: The "B" Tool; Invited speaker: J. R. Abrial (France)
Specification of an Operating System Kernel: FOREST and
VDM Compared; S. J. Goldsack (Imperial College, London, UK)
1100-1230
Session A: Compiler Prototyping with VDM and Standard ML; R. D. Arthan
(ICL, Winnersh, UK)
VDM Development with Ada as the Target Language; David O'Neill
(Generics, Dublin, Ireland)
NUSL: An Executable Specification Language Based on Data
Abstraction; XinJie Jiang, YongSen Xu (Nanjing Normal and
Shantou Universities, China)
Session B: A Three-valued Logic for Software Specification and Validation;
Beata Konikowska, Andrzej Tarlecki, Andrzej Blikle
(Polish Academy of Sciences)
Three-valued Predicates for Software Specification and
Validation; Andrzej Blikle (Polish Academy of Sciences)
1400-1530
Session A: A Support System for Formal Reasoning: Requirements and Status;
C. B. Jones, P. A. Lindsay (University of Manchester, UK)
The Use of VDM within the Alvey Flagship Project; Graham Boddy
(ICL, Manchester, UK)
The Formal Definition of Modula-2 and its Associated Interpreter;
D. J. Andrews, A. Garg, S. P. A. Lau, J. R. Pitchers
(University of Leicester, UK)
Session B: A Set-Theoretic Model for a Typed Polymorphic Lambda Calculus.
A Contribution to Metasoft; Andrzej Borzyszkowski, Ryszard
Kubiak, Stefan Sokolowski (Polish Academy of Sciences)
Mutually Recursive Algebraic Domain Equations; Anne Elisabeth
Haxthausen (Technical University of Denmark, Lyngby)
1600-1730
Session A: Test Case Selection Using VDM; G. T. Scullard (ICL, Manchester, UK)
The VIP VDM Specification Language; Kees Middelburg
(PTT, Leidschendam, Netherlands)
SAMPLE -- A Functional Language; M. Jaeger, M. Gloger, S. Kaes
(TH Darmstadt, Germany)
Session B: Proof Rules for VDM Statements; Robert Milne (STC, Harlow, UK)
Muffin: A User Interface Design Experiment for a Theorem
Proving Assistant; Cliff B. Jones, Richard Moore (University
of Manchester, UK)
Day 3: September 16, 1988 (Friday)
0900-1030: The RAISE Method; C. W. George (STC, London, UK)
The RAISE Specification Language; S. U. Palm (DDC, Denmark)
Semantics of the RAISE Specification Language; K. Ritter Wagner,
K. Havelund (DDC, Denmark)
1100-1230: Correctness Proofs for Meta IV Written Code Generator
Specifications Using Term Rewriting; Bettina and Karl-Heinz
Buth (Christ.-Albrechts-Univ., Kiel, Germany)
Using VDM with Rely and Guarantee-Conditions. Experiences from
a Real Project; J. C. P. Woodcock, B. Dickinson (Oxford Univ.
and GEC, Coventry, UK)
1400-1530: Software Support for the Refinement of VDM Specifications;
P. Kilpatrick, P. McParland (The Queen's Univ. of Belfast, UK)
The Use of VDM in the Specification of Chinese Characters;
Ghee S. Teo, Micheal Mac an Airchinnigh (Trinity College,
Dublin, Ireland)
1600-1730: Nuclear Reactor Protection Software: An Application of VDM;
S. J. Sadler (Rolls-Royce, UK)
Panel
Sponsors of the VDM-Europe Symposium 1988:
CRAI (Consorzio per la Ricercare e la Applicanzione di Informatica, Italy)
GEC (General Electric Company, UK)
GMD (Gesellschaft fuer Mathematik und Datenverarbeitung, Germany)
ICL (International Computer Ltd., UK)
ND (Norsk Data, Germany)
Praxis (UK)
STC (Standard Telephone and Cables, UK)
TFL (Telecommunications Research Lab., Denmark)
Practical Information:
Accommodation:
Attendees may stay at Trinity College. Accommodation consists of either
single rooms or double apartments comprising a lounge and two single
bedrooms. Full Irish breakfast is included in the accommodation fee.
Accommodation is available from 10 September (after 1600) until
18 September (after breakfast).
Fee per night: 35ECU.
**Bookings for accommodation can only be accepted if the registration
form and the full payment are received before August 15.**
If you want to reserve your own hotel contact:
I.T.B., Baggot Street Bridge, Dublin 2, Ireland. tel: +353 1 765871
Registration fee:
The registration fee for the conference includes the proceedings. The
fee for the tutorial includes the book "Systematic Software Development
Using VDM" by C. B. Jones and reprints of volumes I-II-III of the book
"Software Architectures and Programming Systems Design" by D. Bjoerner.
Lunches and coffee or tea during the session breaks are also included.
The conference fee also includes a social event to be organized on
Wednesday evening (14 September).
Conference fee:
250 ECU (225 ECU if payment is received before 15 August)
Tutorial fee:
175 ECU (150 ECU if payment is received before 15 August)
Symposium fee (tutorial and conference):
350 ECU (300 ECU if payment is received before 15 August)
All advance payments should be made to Generale de Banque/Generale
Bank, Brussels, account 210-0806440-34, under name VDM-Europe.
Care should be taken that any costs associated with these payments are
covered by the person registering. Proof of payment will be provided
upon request.
Registration fees can be paid at the Symposium, but, as noted above,
accommodation fees must be received by 15 August.
Registration Form:
Name: _________________________________________________________________
Affiliation: __________________________________________________________
Address: ______________________________________________________________
_______________________________________________________________________
Postal Code: __________________ Country: _____________________________
Phone No.: ____________________ Telex No.: ___________________________
Telefax No.: __________________
I will attend the Tutorial: YES NO
I will attend the Conference: YES NO
I wish to stay at Trinity College: YES NO
If YES: date/time of arrival: ___________________________
date/time of departure: _________________________
I have paid the equivalent of ___________ ECU to the Generale de Banque/
Generale Bank, Brussels, account 210-0806440-34, under name VDM-Europe,
on ___________________ (date).
Signature: ____________________________________
Date: ____________________________________
Please send the registration form to:
Karel De Vriendt
Commission of the European Communities
200 rue de la Loi - A 25 7/3
B-1049 Brussels
Belgium
Tel: +32 2 235 77 69
Telex: COMEU B 21877
Fax: +32 2 235 65 02
E-mail: karel_de_vriendt@eurokom.ucd.ie
Further information is also available from:
Lynn Marshall
VDM'88 Programme Committee Chairman
Unite d'Informatique
Universite Catholique de Louvain
Place Sainte-Barbe 2
B-1348 Louvian-la-Neuve
Belgium
Tel: +32 10 47 31 13 (or +32 10 47 31 50)
Telex: 59037 ucl b
Fax: +32 10 45 03 45
E-mail: lm@lln-cs.uucp (or ...!mcvax!prlb2!lln-cs!lm)