Formal reasoning for fault-tolerant systems
Speaker: Larissa Meinicke, ITEE
When: 2003-08-12 14:00:00
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)