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:

• Static Semantics
• The Domain Universe
• Dynamic Semantics

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

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

-- PeterGormLarsen - 18 Jul 2007