Bill Stoddart's Home Page
Bill's motto: "he believes that all knowledge can be gleaned from a thorough study of the letters of the alphabet."
Recent Papers (1996 onwards)
The articles available from this page are in 600dpi Postscript format. Steve Dunne and Andy Galloway were my co-authors for most of them. Copyright is with the author(s) and others. Individual copies may be taken for study purposes only.
Papers on the Event Calculus.
The Event Calculus is a notation for modelling event driven and real time systems using diagrams plus Z. It uses a theory of communicationg state machines, and makes extensive use of diagrams. Case studies included in the following papers include a distributed seat booking system with timeouts and multiple concurrent booking sessions, and an order processing system. Extensions for modelling hybrid systems provide state machines that evolve in continuous time, and allow a model to include the behaviour of its physical environment, even when this is modelled using continuous mathematics.
- An Introducation to the Event Calculus.
eczum97.ps
- The Event Calculus: Modelling Real Time Systems using
Diagrams and Z.
tees-scm-01-96.ps
- The Event Calculus: Extensions for Modelling Hybrid Systems.
tees-scm-02-96.ps
- An Event Calculus Treatment of the Invoicing of Orders.
Contribution to a series of case studies written to an
outline spec. provided by Henri Habrias of the University
of Nantes.
invoice.ps
- An Event Calculus Model of the Forth Programming System.
eforth97.ps
Papers on Partial Functions and Logic.
Partial functions are used in several formalisms, including Z, B and VDM. They give rise to undefined terms, which occur when a function in applied to a value which is not in its domain. Mark Saaltink has reported (at ZUM'96) that of 400 published Z specifications examined, there were none that did not contain errors due to undefined terms. In these papers we examine the semantics and associated proof theories of systems using partial functions and classical logic. Topics include: historical survey (1905 onwards); denotational semantics of function application, common errors, comparative examples, proof theories, two and three valued logics, partial functions and fixed point theory, and partial functions and predicate transformers.
Papers on Integrating Process Algebra and Z.
- An Operational Semantics for ZCCS (a dialect of value
passing CCS that employs Z as its value calculus).
iceccs.ps
- Integrated Formal Methods.
irin-128andinforsid97.ps
Papers on the Theory of Predicate Transformers
- Extending B's Generalised Substitution to Model
Semi-Decidable Operations.
hypersubs.ps
Papers on Formal Aspects of the Forth Programming Language
- An Event Calculus Model of the Forth Programming System.
eforth96.ps
>