Real-Time and Fault-Tolerance - Specification, verification,
refinement and scheduling

Speaker: Zhiming Liu, UNU-IIST, Macao, China
When: 11.00AM, Tue 17 May 2005
Venue: 78-420
Host: Geoff Dromey
Abstract:

  Fault-tolerance and timing have often been considered to be
  implementation issues of a program, quite distinct from the
  functional safety and liveness properties. Recent work has shown how
  these non-functional and functional properties can be verified in a
  similar way.  However, the more practical question of determining
  whether a real-time program will meet its deadlines, i.e., showing
  that there is a feasible schedule, is usually done using scheduling
  theory, quite separately from the verification of other properties
  of the program. This makes it hard to use the results of scheduling
  analysis in the design, or redesign, of fault-tolerant and real-time
  programs.  In this talk we show how fault-tolerance, timing, and
  schedulability can be specified and verified using a single notation
  and model.  This allows a unified view to be taken of the functional
  and nonfunctional properties of programs and a simple
  transformational method to be used to combine these properties.  It
  also permits results from scheduling theory to be interpreted and
  used within a formal proof framework.  The notation and model are
  illustrated using a simple example.

Biography:

  Zhiming Liu was born and grew up in China. He worked as a researcher
  at the University of Warwick (UK) during 1988-1994, where he also
  obtained his PhD in Computer Science in 1991. He has been a lecturer
  at the University of Leicester (UK) since 1994. He joined the
  International Institute for Software Technology of the United
  Nations University (UNU-IIST) as a research fellow in July 2002.
  Zhiming Liu's research interest is in the area of formal techniques
  for computer systems development with an emphasis on Real-Time and
  Fault-Tolerant Systems, Component and Object systems.