The 10th Overture Workshop

10th Overture Workshop on VDM, Conservatoire National des Arts et Métiers (CNAM), Paris, France, 28 August 2012

Part of FM2012

The 10th Overture Workshop on VDM was held in Paris, France, on Tuesday 28 August 2012. The aim of the workshop was to identify and encourage new collaborative research, and to foster current strands of work towards publication in the mainstream conferences and journals. VDM is one of the longest established formal methods, having its origins in compiler development work in IBM in the 1970s. In the 1990s, the basic VDM modelling language was standardized by ISO and the first commercial tools emerged. Since 2000, the method has been extended to support object-orientation, concurrency, real-time and distribution. A notable recent advance has been the use of VDM as a base language for modelling systems-of-systems (SOS) COMPASS.

The community-based Overture initiative is developing an industry-strength tool on a new open platform, exploiting research mainly in Denmark, the UK, the Netherlands and Portugal. Research in Overture is making advances in proof support and the need to interface VDM models of discrete event systems with heterogeneous models from other engineering disciplines, such as continuous time models of controlled plants Destecs.

The Overture initiative held its first workshop at FM’05. Workshops were held subsequently at FM’06, FM’08 and FM’09, FM’11 and in between. The most recent (9th) workshop, co-located with FM’11, included several reports of development in control and embedded systems design. The 10th Overture workshop emphasized topics that mesh closely with the themes of FM 2012 itself, particularly application experience in industry, validation of tools and methods and the development of tools.

Program

The morning program consisted of an introduction given by Nico Plat (Slides), followed by a number of paper presentations. These included:

• “The Co-Simulation of a Cardiac Pacemaker using VDM and 20-sim” (Carl Gamble, Martin Mansfield, and John Fitzgerald) Slides
• “Supporting the Partitioning Process in Hardware/Software Co-design with VDM-RT” (José Antonio Esparza Isasa, Peter Gorm Larsen and Kim Bjerge) Slides
• “Evolution of the Overture Tool Platform” (Joey Coleman, Anders Kaels Malmos, Claus Ballegaard Nielsen and Peter Gorm Larsen) Slides
• “Towards an extensible core model for Digital Rights Management in VDM” (Rasmus W. Lauritsen and Lasse Lorenzen) Slides
• “Towards a Co-simulation Semantics of VDM-RT/Overture and 20-sim” (Joey Coleman, Kenneth Lausdahl and Peter Gorm Larsen) Slides
• “Initial Report of the Impact of Using Overture/VDM in a Development Process in an Architecture-Oriented Approach” (Shigeru Kusakabe, Yoich Omori and Keijiro Araki) Slides

The afternoon was dedicated to getting hands-on experience with the Overture platform. The intention of this was to get more developers able to (and interested in) actively contributing to the further development of the Overture toolset.

The session was started with a few short presentations:

• “The Overture AST and Plug-in Development” (Kenneth Lausdahl) Slides, Tutorial 1 Java Source, Tutorial 1 VDM Source, Screencase
• “The Inner Workings of Overture-core” (Kenneth Lausdahl) Slides Screencast
• “The build process, using Git and the dependencies” (Joey Coleman). Slides Screencast
• “Next Generation Showtrace” (Peter W.V. Joergensen) Slides
• “State Machines … VDM” (Marcel Verhoef) Slides

After these presentations the workshop participants got the opportunity to get hands-on experience working with development and compilation of different aspects chosen individually by each participant. In this process the core developers helped the participants in order to enable more people to contribute to this Open Source initiative after the workshop.

Proceedings

The proceedings of the workshop are available as a technical report1 from Newcastle University.

Attendees

The workshop attracted 24 attendees in total, from 6 different countries.

Organisers

• Nico Plat (West Consulting BV, NL)
• Claus Ballegård Nielsen (Aarhus University, Denmark)
• Steve Riddle (Newcastle University, UK)

The organizers can be reached via workshop-oc@overturetool.org.

Programme Committee

• Nick Battle (Fujitsu, UK)
• John Fitzgerald (Newcastle University,UK)
• Sakoh Hiroshi (Designers’ Den Corporation, Japan)
• Cliff Jones (Newcastle University, UK)
• Peter Gorm Larsen (Aarhus University, Denmark)
• Claus Ballegård Nielsen (Aarhus University, Denmark)
• Nico Plat (West Consulting BV, The Netherlands)
• Steve Riddle (University of Newcastle, UK)
• Shin Sahara (SCSK Corporation, Japan)
• Marcel Verhoef (Chess IT, The Netherlands)
• Sune Wolff (Terma A/S, Denmark)