Overture Tool
Formal Modelling in VDM
THE 2025 INTO-CPS OVERTURE SUMMIT
incorporating the
23rd Overture Workshop and
3rd INTO-CPS Association Brainstorm
11-12th June 2025 hosted by Aarhus University, Denmark
Programme
9:00-09:30 Tomohiro Oda: Support for Hypothetical Initiation and Dynamic Exploration using History of Operation in ViennaTalk [paper; slides]
9:30-10:00 Tomohiro Oda: Implementing Mutation Testing for VDM-SL in ViennaTalk [paper; slides]
10:00-10:30 Nick Battle and Peter Gorm Larsen: Towards Operation Proof Obligation Generation for VDM [paper; slides]
10:30-11:00 Coffee
11:00-11:30 Leo Freitas, Alastair Pollitt and Patrick Degenaar Modelling the CANDO3 Optrode Command Interface [paper; slides]
11:30-12:00 Leo Freitas, Ben Wooding, Bill Scott, Alastair Pollitt, and Patrick Degenaar: Proving the Correctness of CANDO3 Optrode Command Interface VDM model in Isabelle/HOL [paper; slides]
12:00-12:30 Joe Hare, Leo Freitas, and Ken Pierce: Translating a VDM Model of a Medical Device into Kapture [paper; slides]
12:30-13:30 Lunch
13:30-14:00 Mennatullah Khedr and John Fitzgerald The Composition of Digital Twins for Systems-of-Systems: a Systematic Literature Review [paper; slides]
14:00-14:30 John Fitzgerald, Peter Gorm Larsen, and Claudio Gomes Introductory Courses on Digital Twins: an Experience Report: [paper; slides]
14:30-15:00 Anders Jensen and Giuseppe Abbiati: A flexible finite element tool for digital twin services [paper; slides]
15:00-15:30 Coffee
15:30-17:00 Brainstorming on future of the Overture community
17:00 Close
18:30 Dinner at Food Club, Åboulevarden 30, 8000 Aarhus C, Danmark
Call for Contributions
We are excited to announce that 11-12th June 2025 will see a joint gathering of two groups active in well-founded model-based methods for Systems Engineering at Aarhus University. We encourage both papers and presentations presenting work from initial “brainstorm” ideas to publishable maturity in any of the areas covered.
The Overture Workshop
The Overture Workshop features the Vienna Development Method (VDM), the open-source project Overture, and related tools and formalisms. VDM is one of the best-established formal methods, its modelling languages (VDM-SL, VDM++, VDM-RT) and tools (including VDMTools, Overture, INTO-CPS, ViennaTalk, VDMJ and VDM VSCode) providing a platform for work on modelling and analysis technology that includes IDEs, static and dynamic analysis, test generation, execution support, and model checking. Proceedings of former workshops are available at https://www.overturetool.org/.
The INTO-CPS Association Brainstorm
The INTO-CPS Association Brainstorm is a newer informal event that focuses on multi-modelling, co-simulation, and other technologies for model-based design, implementation and deployment of Cyber-Physical Systems and especially Digital Twins. The focus is on the open INTO-CPS tool chain and associated frameworks. Previous workshops and brainstorm sessions have been invaluable in encouraging both new and established members of the community in their work, helping to determine priorities and future directions.
Important Dates
09th of May 2025 Extended ~25th April 2025~: Submission of papers and outlines of presentations
19th May 2025: Notification to authors
8th June 2025: Final version of papers due
11-12th June 2025: Workshop
Call
Our workshop provides a forum for discussing and advancing the state of the art in Digital twins, formal modelling and analysis using VDM/Overture or INTO-CPS and their associated formalisms and extensions. We warmly welcome contributions on the development of foundations, methods, tools, and reports of practical experience.
We welcome submissions in the following formats:
- Presentation summaries: Short-form summary (max. 2 pages LNCS) of the content of presentations on work that is at an early stage and either addresses an open issue or reports experience in the Overture or INTO-CPS domains.
- Tool reports: Shorter papers focusing on initial results in developing and applying the tools and formalisms, with a view to receiving community feedback ahead of a full paper (to a future workshop or other venue). Tool reports should not exceed 8 pages LNCS and should include a link to (e.g. GitHub), or instructions for, accessing the tool / model being reported on.
- Full papers: Longer papers reporting more mature results. Full papers should not exceed 15 pages LNCS.
Each tool report or full paper will be peer-reviewed by at least three members of the PC. The scope of the workshop includes, but is not restricted to:
- Reports of applications of VDM or INTO-CPS-related technology, especially reports of industrial use.
- Papers describing requirements, designs, implementations, and case studies of VDM or INTO-CPS technology, whether yet implemented or not.
- Papers on foundations and methodology for VDM or INTO-CPS, including the description of real-time, cyber-physical systems, digital twins and systems-of-systems.
- Papers combining VDM with other notations and tools.
- Position papers on VDM and its promotion in industry practice.
- Papers on extensions of VDM-related tools including Visual Studio Code, INTO-CPS assets and ViennaTalk.
Submission
EasyChair: https://easychair.org/conferences/?conf=ovt23
Organising Committee
- Ken Pierce, Newcastle University, United Kingdom (ken.pierce@newcastle.ac.uk)
- Peter Gorm Larsen, Aarhus University, Denmark (pgl@ece.au.dk)
- Leo Freitas, Newcastle University, United Kingdom (leo.freitas@newcastle.ac.uk)
Program Committee (Draft)
- Shaukat Ali
- Stylianos Basagiannis
- Nick Battle
- John Fitzgerald
- Fuyuki Ishikawa
- Hugo Daniel Macedo
- Paolo Masci
- Tomohiro Oda
Contact
All questions about submissions should be emailed to Ken Pierce (kenneth.pierce@newcastle.ac.uk)