The 3rd Overture Workshop
Date and location
Third Overture Workshop
27-28 November 2006
Newcastle University, Newcastle upon Tyne, UK
Background
There was a lot of activity around tools and applications of VDM in
2005-6. However, apart from the tools work, there are several drivers
that lead us to consider new research directions in the semantics and
foundations of VDM’s version of formal, yet lightweight and applicable
methods. The aim of this workshop was to form collaborative links and
concrete plans for research directions related to, but not confined to,
VDM. Topics included:
- Drivers from application areas: distributed systems, concurrency,
real-time.
- Semantics Support: underpinning logics, type theory, static
analysis, proof theory, proof technology.
- Methodological Issues: links to other design formalisms,
interoperability.
Outcomes
We decided to pursue research in three main streams, each of which has a
group:
- Semantics: Initial topics include VDM++ semantics (based on the
definition of a kernel language) and proof theory development. The
group will be convened by John Fitzgerald and will initially include
Bernhard Aichernig, Joey Coleman, Peter Gorm larsen and Jose
Oliveira.
- Tools: The group will be convened by Peter Gorm Larsen.
- Methods and Applications: Bernhard Aichernig and Nico Plat will
convene a group on methods and applications, looking initially at
the links between VDM++ and JML.
Cutting across the activities of the three groups, we will start work on
VDM/Overture approaches to the Grand challenges, with the first of these
being the Mondex study, led by Jeremy Bryans. We will go on to pursue
the Posix fault tolerant file store example next.
Contributed Papers and Presentations
The following papers and presentations are as supplied by their authors.
They have not been subject to peer review. If you have any queries about
externally published materials based on these papers, please contact the
authors directly.
A Review of the VDM-SL Static and Dynamic Semantics, Peter Gorm Larsen,
IHA, Denmark:
- Getting PROSPER Tool Support Usable Again
(Slides) Peter Gorm Larsen, IHA, Denmark
- What Next for VDMTools? Model Checking, Test Case Generation or
Proof? (Slides) Shin Sahara, CSK Systems, Japan
- Reinvigorating pen-and-paper Proofs in VDM: the pointfree approach
(Slides) Jose N. Oliveira, University of
Minho, Portugal
- Proofs using SOS: support tooling (Slides)
John Hughes and Cliff Jones, Newcastle University, UK
- To be or not to be (LPF) (Slides) John
Fitzgerald and Cliff Jones, Newcastle University, UK
- Explicit vs. Implicit Polymorphism in OML
(Slides) Thomas Christensen, University of
Aarhus, Denmark
- Future Proof Dynamic Semantics for Overture
(Slides) Marcel Verhoef, CHESS and Radboud
University Nijmegen, The Netherlands
- Hybrid System Modeling in VDM (Slides)
Marcel Verhoef
- Recent Trends in O-o Modelling Languages JML, rCOS, CREDO
(Slides) Bernhard Aichernig, Graz University
of Technology, Austria
- Overture Architecture & Status (Slides)
Peter Gorm Larsen and Marcel Verhoef
The following paper was sent by Tiago Alves, who could not attend in
person: Sex up Overture
Discussions
See the Discussion Summary for
a record of discussions at the workshop, including a summary of the main
actions.
Participants
- John Fitzgerald, Newcastle: Proof and Proof Support, Non-classical
Logics for Undefinedness.
- Peter Gorm Larsen, IHA, Denmark: VDM Semantics, Tool Support,
Embedded Systems.
- Shin Sahara, CSK, Japan: Future of VDMTools: model checking, test
case generation or proof?
- Marcel Verhoef, ChessIT, Netherlands: Tool Support, Embedded
Systems.
- Nico Plat, West Consulting, Netherlands: Tool Support, Methodology.
- Juan Bicarregui, CCLRC, UK: Verified Software Repository
- Cliff Jones, Newcastle: Proof, Operational Semantics.
- John Hughes, Newcastle: Proof Support
- Joey Coleman, Newcastle: Operational Semantics
- Zoe Andrews, Newcastle: VDM and models of Stochastic Processes
- Jeremy Bryans, Newcastle: VDM, dynamic coalitions, access control
- Richard Payne, Newcastle: dynamic reconfiguration policies
- Thomas Christensen, DAIMI, Denmark: Explicit vs. implicit parametric
polymorphism in OML
- Jose Nuno Oliveira, Minho, Portugal: VDM proof theory and proof
strategies
- Bernhard Aichernig, TU Graz, Austria: Recent Trends in OO Modeling
Languages and relating VDM++ to JML, rCOS and CREDO semantics