Real-Time and Fault-Tolerance - Specification, verification, refinement and scheduling
Speaker: Zhiming Liu, UNU-IIST, Macao, China
When: 2005-05-17 11:00:00
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.
Type: ITEE Seminar
Contact:Geoff Dromey, seminar host (G.Dromey@griffith.edu.au)
or Guido Governatori (ITEE seminar co-ordinator)
(guido@itee.uq.edu.au)