The University of Queensland Homepage
School of ITEE ITEE Main Website

 Seminar: Formal reasoning for fault-tolerant systems

ITEE Ph.D confirmation seminar: Larissa Meinicke, 02.00PM, Tue 12 Aug 2003

Formal reasoning for fault-tolerant systems

Speaker: Larissa Meinicke, ITEE

When: 02.00PM, Tuesday 12 Aug 2003

Venue: 78-622

Host: Prof Ian Hayes

Abstract:

  A fault-tolerant system is one that is capable of performing safely
  or correctly in the presence of faults. Commonly, systems that are
  required to be fault-tolerant are composed of communicating hardware
  and software components that interact with their environment. Such
  systems are likely to have timing constraints. These characteristics
  suggest that reasoning about fault-tolerant systems involves
  reasoning about the interaction between discrete and continuous
  components and real-time constraints. Because most fault-tolerant
  systems are unable to function correctly (or in a fail-safe way)
  under all circumstances it is necessary to be able to reason about
  their reliability. Software reliability is a measure of the ability
  of a software component to satisfy its specification in certain
  operational conditions over a period of time.

  Formal methods may be used to specify, verify and derive programs in
  a mathematically vigorous way. Currently however, formal methods for
  reasoning about continuous concurrent program behaviour are
  underdeveloped compared to methods for reasoning about discrete
  concurrent behaviour. Also, most formal techniques for the
  development of programs do not facilitate reliability reasoning. It
  would be useful to be able to reason formally about system
  reliability in the same framework that that is used to develop and
  verify other program characteristics.

  The aim of this seminar is to construct a formal framework that can
  be used to reason about the behaviour and reliability of
  fault-tolerant systems. Specifically this work will explore ways in
  which the reliability of discrete and continuous real-time
  interacting software components can be expressed and reasoned about.

Biography:

  Larissa Meinicke graduated with a Bachelor of Information Technology
  (with honors) degree from the University of Queensland in 2001. She
  is currently undertaking a PhD program in the area of Formal
  methods.

Type:

Ph.D confirmation

Contact:

Prof Ian Hayes, seminar host (ianh@itee.uq.edu.au)
or Guido Governatori (ITEE seminar co-ordinator) (guido@itee.uq.edu.au)

ITEE seminar web page: http://www.itee.uq.edu.au/~seminar


[All seminars]