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.
Contents
-
Readings
-
Talks
-
Models
-
Software
-
Teaching
Readings
We have readings on IrishVDM in various formats
(for PDF format, a
free Acrobat Reader
is available).
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:
-
The 1990 PhD Thesis of Dr. Mcheal Mac an Airchinnigh, "Conceptual Models
and Computing"
(PDF, 2377k).
-
The 1995 version of the "Formal Methods and Testing" Tutorial
(PDF, 857k)
-
The 1997 PhD Thesis of Dr. Gerard O'Regan, "Applying Formal Methods
to Model Organizations and Structures in the Real World"
(DVI, 769k)
(PS, 1449k)
(PDF, 1320k)
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 2000 PhD Thesis of Dr. Arthur Hughes,
"Elements of an Operator Calculus"
(PDF, 1233k)
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
ISCM.sty
)
and
Irish VDM Technical Reports
.
Talks
-
10 minute Presentation
at VDM Open Session, 20th Sep. 1999, FM'99, Toulouse.
-
2 hour Presentation to TU-Graz, Austria,
19th May 2000
(DVI, 143k)
(PDF, 305k)
(PS, 1819k)
.
-
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
(DVI, 144k)
.
Models
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
specific sub-trees.
The model describes operations for creating and modifying tree cursors,
as well as proofs of correctness and key properties
(July 27th 2001).
(DVI, 100k)
(PDF, 180k)
(PS, 196k)
Teaching
We have some teaching materials available
These are not fully complete at present.
This page was was last updated
12:20 03/05/02
by Andrew Butterfield.