VDM++ Crash Course - 1999/2000
[ DI/UM ]

Lecturer

Dr. P.G. Larsen (IFAD )

Course Schedule

1.

Introduction and Overview of VDMTOOLS®

• IFAD profile
• The VDM technology
• Client experiences
• Tools overview

2.

Alarm Example

• The process of going from informal requirements to a formal model
• Getting a first glimpse of a VDM++ specification
• Gaining familiarity with the tools

3.

Object-Oriented Modelling in VDM++

• Object-orientation
• OO concepts in VDM++
• Rose -VDM++ Link, round-trip engineering with UML
• Concurrency in VDM++

4.

Types, functions and expressions

• Gaining experience of the types available in VDM
• Learning how to specify functions
• Experience the richness of VDM 's language of expressions

5.

Statements

• Learning how the internal state of an object may be manipulated
• Range of statements available to perform such manipulation

6.

Further Examples

• Store example
• Gateway example
• Tracker example
• Traffic Light Control

7.

Test Environment

• Using batch scripts models may be automatically tested
• Such testing is repeatable and systematic
• Test coverage information may be accumulated

8.

Advanced functions

• VDM++ provides facilities for specifying more sophisticated functions
• Polymorphic functions
• Higher-order functions
• Polymorphic higher-order functions

9.

VDM to C++ Code Generator

• Understanding the potential and limitations of the VDM to C++ code generator
• The structure of the code generator
• Learning to use the code generator

10.

Conclusions

• Further reading
• Technology extensions
• Course evaluation

Bibliography

FL98

J. Fitzgerald and P.G. Larsen.
Modelling Systems: Practical Tools and Techniques in Software Development .
Cambridge University Press, 1st edition, 1998.

Jon86

C. B. Jones.
Systematic Software Development Using VDM .
Series in Computer Science. Prentice-Hall International, 1986.
C. A. R. Hoare.

Da-

John Dawes.
The VDM-SL Reference Guide.

AD-

Derek Andrews, Darrel Ince.
Practical Formal Methods with VDM.

L*-

John Lathan, Vicky Bush, Ian Cottam.
The Programming Process.

Ca-

Chris Casey.
A Programming Approach to Formal Methods.

B*-

Bicarregui, Fitzgerald, Lindsay, Moore, Ritchie.
Proof in VDM: A Practitioner's Guide.

Return to EDFS 's main page. Outras disciplinas leccionadas pelo DIUM