Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Wed, 4 Nov 92 14:24:36 GMT
From: Mike.Gordon@uk.ac.cam.cl
Message-Id: <9211041424.AA00418@dipper.cl.cam.ac.uk>
To: info-hol@edu.uidaho.cs.ted
Subject: Draft paper on real-time


The main deliverable of the SAFEMOS project is a book entitled
"Towards Verified Systems" to be edited by Jonathan Bowen of the PRG
at Oxford. A first draft of my chapter in this book, entitled
"Verifying real-time programs: a case study", is available as the
file:

   STAPaper.ps.Z 

by anonymous FTP from 

   ftp.cl.cam.ac.uk 

in the directory 

   hvg/papers.

The chapter will be reviewed and I expect to produce a final version
early next year. I would welcome comments and/or suggestions before then.

Here is an overview of the chapter:

   The temporal behaviour of programs that interact with
   their environment depends on the compiler used and the timing
   characteristics of the host processor. Working out the details can be
   messy. As part of the SAFEMOS project, an approach to managing this
   complexity based on special-purpose theorem proving tools, has been
   developed.  Specifications are written in a state transition notation
   annotated with real-time constraints.  Implementations are programs
   coded in a simple imperative language with assignments, conditionals,
   asynchronous inputs, wait-statements, while-commands and
   forever-loops.  The meaning of programs is defined by a translation to
   sequences of machine instructions, but automated tools can derive
   behavioural abstractions that enable reasoning to be conducted near
   the source program level. A set of rules, combining aspects of Hoare
   logic and temporal logic, has been derived. This chapter is centered
   around an example consisting of a four-phase handshake (using two
   wait-loops) followed by an iterative numerical computation (using a
   while-loop).  This example has been chosen to show how reasoning about
   timed interactions with the environment can be combined with the use
   of conventional verification conditions.


Mike Gordon