Training Material

Teaching Material for “Modelling Systems”

We have prepared a set of slides (Microsoft Powerpoint) that can be used for teaching VDM, based on the first edition of the book. It is encouraged to combine the lectures with practical exercises (home work assignments) using Overture or VDMTools Lite which can be downloaded for free from www.vdmtools.jp/en. Teachers are welcome to download and review the material available here. Any use of this material must include acknowledgement of the authors.

The slide collection contains slides for:

• Introduction Chapter 1
• Constructing a Model Chapter 2
• Describing System Properties Using Logical Expressions Chapter 4
• The Elements of a Formal Model Chapter 5
• Sets Chapter 6
• Sequences Chapter 7
• Mappings Chapter 8
• Recursive Structures Chapter 9
• Validating Models Chapter 10

Teaching Material for “Validated Designs for Object-oriented Systems”

We have prepared a set of slides (Microsoft Powerpoint) that can be used for teaching VDM++, currently covering chapter 1 to 8 of the book. Each file corresponds roughly to a one hour lecture. The course material uses the examples from the book. It is encouraged to combine the lectures with practical exercises (home work assignments) using Overture or VDMTools Lite.

The slide collection contains slides for:

• Introduction and process
• VDMTools and Logic
• Defining data and functionality
• Modelling unordered collections
• Modelling ordered collections
• Modelling relationships
• Introduction and the connection between UML and VDM++
• Concurrency
• Real-time Development in VDM++ Seperate guidelines for the newest VICE extensions to VDMTools.
• Model quality

Download: slide bundle

Other

Slides:

• The satisfiability proof obligations for implicitly defined functions/operations
• statebased modelling
• A small tutorial for introducing newcommers to VDMTools
• Dines Bjørner’s VDM overview

Validation Course

Validation Course (New - July 2000) This course was developed for use at the Technical University of Wroclaw in Poland during 2000 as part of a Socrates Teaching Staff Mobility sponsored by the European Union. Validation Course (62 slides)