Venue & Time:
============

Room 202
Building E6A, Macquarie University
12:00 noon

Talk Abstract
=============

I will briefly introduce myself and the people I am working with at
the ANU, and then present two recent conference papers on formal
semantics for UML.  In "Improving the Definition of UML" I study the
role of UML, and establish 6 criteria for a good definition of the
language.  The current definition is evaluated and found wanting.  I
then survey the UML formalisation literature in the light of the
criteria.  The other paper "Dynamic Logic Semantics for UML
Consistency" proposes a translation from UML into dynamic logic (which
will be introduced gently!).  This allows us to use a tableau theorem
prover to check for model satisfiability.  The translation achieves a
higher level of abstraction for sequence diagrams than previous
formalisation proposals.  I will conclude with a few ideas about my
post-doctoral work in the hopes of generating some interesting
discussion.


Speaker-bio
===========

Before taking any tertiary education, Greg worked for 12 years at the
Department of Social Security (now Centrelink) mostly in mainframe
operations and integration testing.  In 1997 he became a full-time
student at the University of Tasmania, completing his BSc with double
major in mathematics in 1999, and BSc(hons) in maths in 2001.
Attracted by formal logic, he joined the the Automated Reasoning Group
at the Australian National University as a PhD student, and began
working on a readable formalisation of category theory in higher order
logic.  It then occurred to him that even informal category theory is
completely unreadable, and that the proposed formalisation would be
unlikely to have a positive impact on anybody's daily life.  Now he
has almost completed his PhD thesis on formal semantics for UML, which
he hopes will bring the precision of formal logic to the work of
software developers and business analysts.