Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

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 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:

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

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

Programme Committee