The 13th Overture Workshop

Proceedings

The proceedings for this workshop can be found at

Programme

9:00-9:15 Opening, Peter Gorm Larsen and Fuyuki Ishikawa

9:15:10:00 Invited Talk: Taro Kurita, Sony Felica

10:00-10:30 Break

10:30-12:30

• JODTool on the Overture Tool to manage formal requirement dictionaries, Yoichi Omori, Keijiro Araki and Peter Gorm Larsen
• VDM Animation for a Wider Range of Stakeholders, Tomohiro Oda, Yasuhiro Yamamoto, Kumiyo Nakakoji, Keijiro Araki and Peter Gorm Larsen
• Integrating the PVSio-web modelling and prototyping environment with Overture, Paolo Masci, Luis Diogo Couto, Peter Gorm Larsen and Paul Curzon
• Extending the Overture code generator towards Isabelle syntax, Luís Diogo Couto and Peter W. V. Tran-Jørgensen

12:30-14:00 Lunch

14:00-15:30

• Code Generation of VDM++ Concurrency, Georgios Kanakis, Peter Gorm Larsen and Peter W. V. Tran-Jørgensen
• Generating Java RMI code for the distributed aspects of VDM-RT models, Miran Hasanagic, Peter Gorm Larsen and Peter W. V. Tran-Jørgensen
• Improving Time Estimates in VDM-RT Models, Morten Larsen, Peter Würtz Vinter Tran-Jørgensen and Peter Gorm Larsen

15:30-16:00 Break

16:00-17:30

• Case Studies on Combination of VDM and Test-Driven Approaches: Application, Model Finding and Refinement, Fuyuki Ishikawa
• Pacemaker Parameter Tuning using Crescendo, Carl Gamble, Martin Mansfield, John Fitzgerald and Peter Gorm Larsen
• TASTE for Overture to keep SLIM, Marcel Verhoef and Maxime Perrotin

17:30-17:45 Closing including discussions about future

CALL FOR PAPERS

The 13th Overture Workshop will be held on the 23rd June 2015 in connection with the Formal Methods 2015 symposium

This is the 13th in a series of workshops on the Vienna Development Method (VDM) seen in the open-source Overture setting. Although VDM is one of the oldest formal methods to have enjoyed a level of industry use, it nevertheless has a lively and youthful research community, which has grown up around the development of the Overture open tools platform. On top of the Overture platform the Crescendo and Symphony tools from respectively the DESTECS and COMPASS projects, as well as the new development that will take place in the new INTO-CPS project (see http://into-cps.au.dk/). The platform provides a vehicle for activity in modelling and analysis technology including static analysis, interpreters, test generation and execution support and model checking. The growth of this community has been greatly assisted by the Overture workshop series.

There is a long tradition for having these workshops co-located with the FM symposia (2005, 2006, 2008, 2011 and 2012). We did not collocate with the FM’14 symposium in Singapore since we felt that it would be hard to gather enough attendance so instead John Fitzgerald, Ken Pierce and Peter Gorm Larsen delivered a Crescendo tutorial (see http://crescendotool.org/). Proceedings of previous workshops may be obtained from https://www.overturetool.org/.

Call for Papers

Our workshop aims to provide a forum for discussing and advancing the state of the art in formal modelling and analysis using VDM and its family of associated formalisms including extensions for distributed and real-time systems. We strongly welcome contributions on the development of tools for VDM as well as developments in foundations and reports of practical experience. The page limit is 15 pages.

The scope of the workshop includes, but is not restricted to:

• Reports of applications of VDM technology, especially reports of industrial use.
• Papers describing requirements, designs, implementations and case studies of support tools for VDM, whether or not implemented on the Overture open tools platform.
• Papers on the foundations and methodology associated with VDM and its extensions, including the description of real-time and distributed systems.
• Papers combining VDM with other notations and tools.
• Position papers on VDM and its promotion in industry practice.
• Papers on extensions of Overture including Crescendo, Symphony and VDMPad.

Important Dates

• 1st April

  Extended to 7th April 2015: Submission deadline for workshop papers (submit at https://easychair.org/conferences/?conf=overture13)

• 1st May 2015: Notification to workshop paper authors
• 1st June 2015: Final version of workshop papers due

Organisers

• Fuyuki ISHIKAWA, National Institute of Informatics, Japan
• Peter Gorm LARSEN, Aarhus University, Denmark

The organising committee can be reached via the following e-mail address: workshop-oc@overturetool.org

Program Committee

• K Araki, Kyushu University, Japan
• N Battle, Fujitsu, UK
• J S Fitzgerald, Newcastle University, UK
• T Oda, Software Research Associates, Inc., Japan
• JN Oliveira, Minho University, Portugal
• N Plat, West Consulting, Netherlands
• V Stolz, Oslo University, Norway
• M Verhoef, European Space Agency, Netherlands

Participants