Irish School of VDM
The "Irish School of VDM" is a branch of the Vienna Development Method
(VDM) that has concentrated its research activity on exploiting the mathematical
concepts of structure in order to develop operator calculi for building
and resoning about models in VDM. The work should be viewed as being complementary
to the work in model-theoretic formal methods such as standard VDM (VDM-SL)
and Z, rather than as a competitor.
We have readings on IrishVDM in various formats
(for PDF format, a
free Acrobat Reader
The following cover the early period
(1987-1997), when research focussed on structures such as semigroups, monoids,
groups and their morphisms as a foundation for the calculi:
More recent work has looked at generalising the structures involved, to
the concepts of inner and outer laws, which admit partiality in a natural
way, as well as a major move into adopting category theory as a key foundation
for the calculi. We have a particular interest in exploring the category-theoretic
concept of topos as a cornerstone of the Irish VDM. Topoi are categories
which are "set-like" and come equipped with a (ready-made) Heyting logic.
Available material includes:
The 1990 PhD Thesis of Dr. Mcheal Mac an Airchinnigh, "Conceptual Models
The 1995 version of the "Formal Methods and Testing" Tutorial
The 1997 PhD Thesis of Dr. Gerard O'Regan, "Applying Formal Methods
to Model Organizations and Structures in the Real World"
The 2000 PhD Thesis of Dr. Arthur Hughes,
"Elements of an Operator Calculus"
A very rough draft version of an "Irish VDM Reference"
(PDF, 1,017k) is available.
At this point in time it may raise more questions than it answers, however.
All feedback is welcome --- send to Andrew.Butterfield @ cs.tcd.ie .
Online resources include
TeX stuff for Irish VDM
(the main style file being called
Irish VDM Technical Reports
10 minute Presentation
at VDM Open Session, 20th Sep. 1999, FM'99, Toulouse.
2 hour Presentation to TU-Graz, Austria,
19th May 2000
45 minute overview of Topos Logic, as part of 90-minute tutorial
during 5th Irish Workshop in Formal Methods (IWFM'01),
held in Trinity College, Dublin, 16th-17th July 2001
We include links to documents decribing various models
written using Irish VDM.
"Trees and Cursors",
a model of tree-cursors which can be used to identify
The model describes operations for creating and modifying tree cursors,
as well as proofs of correctness and key properties
(July 27th 2001).
We have some teaching materials available
These are not fully complete at present.
This page was was last updated
by Andrew Butterfield.