Welcome!
The first ESPRIT ProCoS-WG Working Group workshop was held at Gentoft, Denmark in January 1994. An "active" photograph of the participants is available. You can point to some of the participants for further information about them.
ProCoS-WG also supports Z User Meetings organized by the Z User Group, concerned with the Z notation and the B method. In addition, information is available on formal methods in general as part of the World-Wide Web (WWW) Virtual Library.
Joan Arnold is available if you have any secretarial requirements or queries about the meeting. Jonathan Bowen may also be able to help you. Tony Hoare leads ProCoS and He Jifeng is a researcher on the ProCoS II project. Financial queries may be directed to the administrator, Mike Field.
If you are interested in ProCoS and wish to join the mailing list, please email your contact details to procos-list-request@comlab.ox.ac.uk
Please find below a timetable of events for Tuesday and Wednesday, together with a list of presentations with brief summaries. The talks are in Room 051 of the Wolfson Building. Refreshments are available on the basement social area close by. All "locals" are also welcome to attend individual or all talks - no registration is necessary.
9.00 am Coffee available
9.30 am Welcome
9.35 am Martin Fränzle
Towards a Sound Digitality Abstraction
10.15 am Markus Müller-Olm
A Modular Codegenerator Proof by Stepwise
Abstracting the Machine
11.00 am Coffee
11.30 am Burghard von Karger
The Sequential Calculus
12.30 pm Lunch
2.00 pm He Jifeng
A Probability Model for the Guarded Command
Language
2.45 pm Ben Moszkowski
Some Aspects of Temporal Compositionality
3.15 pm Coffee
3.45 pm Egon Börger
Proof of Correctness of a Scheme for
Compilation of occam programs on the Transputer
4.25 pm Joakim von Wright
Refinement Calculus with Window Inference
4.55 pm Announcements
5.00 pm Close
7.30 pm Drinks, Worcester College
8.00 pm Dinner
9.00 am Coffee available
9.30 am Augusto Sampaio
Towards Provably Correct Hardware/Software
Partitioning using occam
10.00 am Job Zwiers
Layering of Real-Time Distributed Processes
10.30 am Mads Dam
Model Checking General Processes
11.00 am Coffee
11.30 am John Herbert
Appropriate Formal Methods
11.45 am Discussion Session including:
Ben Moszkowski
Compositional proof techniques for continuous
time
12.30 pm Lunch
2.00 pm Brief informal presentations by:
ProCoS project site leaders
Thomas Lindner
Peter Lucas
Fernando Mejia
Olaf Owe
etc.
3.15 pm Tea
3.45 pm Open Session - future plans
ESPRIT Framework IV etc.
5.00 pm Close.
Prof. Dr. Egon Börger, Dipartimento di Informatica, Universita di
Pisa, Italy.
Brief Summary of Presentation:
We develop several models of occam at different levels of
compilation by Transputer instructions. We relate them by
relative correctness proofs, providing altogether a transparent
mathematical correctness proof for a general compilation scheme of
occam programs on the Transputer. We start from the
formal model developed by us last year which was still close to
the abstraction level of atomic occam commands and reach a
formal model of the Transputer Instruction Set Architecture. We
use evolving algebras as a specification tool.
Length of presentation: 30-40 minutes
Dr. Ben Moszkowski, Department of Electrical and Electronic
Engineering, Merz Court,
University of Newcastle upon Tyne.
Brief Summary of Presentation:
We discuss how to compositionally specify and reason about some
important temporal phenomena.
Length of presentation: 30 minutes
Olaf Owe, University of Oslo visiting
Oxford University.
Brief Summary of Presentation:
From one observation, one can not observe whether a
program/process/object is deterministic or not. This suggests that a
non-deterministic object should be specified as if deterministic.
Moreover it motivates the concept of non-deterministic functions,
often used informally in computer science.
These ideas are formalized in a logical framework for reasoning about
concurrent objects (with internal and external
non-determinism). Our framework allows equational reasoning of
non-deterministic functions, even though it is possible to specify
non-determinism. We give a consistent and complete set of proof rules
for a small specification language.
Length of Presentation: short
Markus Müller-Olm,
Kiel University, Germany.
Brief Summary of Presentation:
Starting from a low level semantics of a machine-language, more
abstract descriptions are derived by calculation. This enables to
modularly bridge the gap between detailed description of machine
behaviour and less specific demands of higher level programming
languages when proving code generators correct.
Length of Presentation: 30-45 minutes
Martin Fränzle, Kiel University, Germany.
Brief Summary of Presentation:
Testing preorders are applied to prove soundness of a digital
abstraction of switching circuitry.
Length of Presentation: 30 minutes + discussion
Burghard von Karger, Kiel University, Germany.
Brief Summary of Presentation:
The sequential calculus is an algebraic calculus like the relational
calculus, for reasoning about sequential phenomena. We show its
application to temporal logic and the design of reactive systems.
Length of Presentation: 60 minutes
Assoc. Prof. Joakim von Wright,
Åbo Akademi University, Finland.
Brief Summary of Presentation:
The
Refinement Calculus supports local transformations of large
program terms. The
HOL theorem prover can be used as a platform for a
Refinement Calculator which formally proves refinements correct.
Length of Presentation: 30 minutes
Augusto Sampaio, University of Pernambuco, Brazil.
Brief Summary of Presentation:
I will present some ideas towards an approach to provably
CORrect hardware/software partitioning. We use occam as
the source programming language and perform the partitioning by
applying a series of algebraic transformations on the source
program. The result is still an occam program; its structure
reflects the hardware and software components, and how they interact
to achieve the overall goal. A simple case study is developed to
illustrate the partitioning and to show how the transformations can be
proved to preserve an algebraic semantics of occam.
Length of Presentation: 20 minutes
Job Zwiers,
University of Twente, The Netherlands.
Brief Summary of Presentation:
An assertional proof system is proposed for a shared variable
language extended with real-time constructs and synchronization,
and a layering operator. The proof system is used to check real-time
side conditions for an extended Communication Closed Layers rule.
Reversely, this rule extends the scope of applicability of the proof
system. The resulting system combines algebraic and assertional
reasoning. A number of small examples are discussed.
Length of Presentation: 30 minutes
Dr. John Herbert, SRI Cambridge and
Cambridge University.
Brief Summary of Presentation:
The use of appropriate
formal methods, in terms of notations, proof
tools, interfaces both semantic and syntactic, is discussed.
Reference is made to relevant work at SRI Cambridge and the University
of Cambridge Computer Laboratory.
Length of presentation: 10 minutes
Mads Dam,
SICS, Sweden.
Brief Summary of Presentation:
We present a compositional proof system for checking processes
against formulas in the model µ-calculus which is capable of
handling general infinite state processes.
Length of Presentation: 30 minutes
Thank you for attending the meeting. If you are staying on in Oxford or
elsewhere in the UK, further
on-line information is available. For your convenience, the X70 coach timetable to
Heathrow and Gatwick airports is also provided on-line.
This page is accessible on-line under the following "URL"
(Uniform Resource Locator):
Proof of correctness of a scheme for compilation of occam
programs on the Transputer
Some aspects of temporal compositionality
A Logical Framework for Concurrent Objects
A Modular Codegenerator Proof by Stepwise Abstracting the Machine
Towards a sound digitality abstraction
The Sequential Calculus
Refinement Calculus with Window Inference
Towards Provably Correct Hardware/Software Partitioning using
occam
Layering of Real-Time Distributed Processes
Appropriate Formal Methods
Model Checking General Processes
Topics for Discussion
Ben Moszkowski - Compositional proof techniques for continuous time
Prepared by
Jonathan Bowen
as part of the ProCoS archive.
Comments and requests are welcome.