Software Model Checking
Speaker: Dr Kirsten Winter, SVRC
When: 2003-01-30 11:15:00
Venue: 78-420
Host: Associate Professor David Carrington
Abstract:The aim of formal methods is to support modelling and analysis of
software and hardware artifacts. Model checking is an automatic
verification technique that has proven successful for analyzing
complex digital hardware designs in real industrial
applications. Consequently, there is a growing research interest in
applying this technique to the analysis of software systems.
Being a fully algorithmic approach that runs without user
interaction, model checking is appealing for use in industry. Any
temporal logic property -- concerning the control flow of a system
-- can be checked as long as the system is finite and small enough
for an exhaustive search in the state space. Since model checking
was originally developed for the needs of hardware verification, the
accompanying notations are not suitable for modelling software.
This talk will propose an interface from a higher-level
specification language to a model checker in order to support the
modelling of software systems. Specifically, I will introduce my
work on model checking for a high-level formal language called
Abstract State Machines (ASM) and illustrate it by means of the
results of an industrial case study. The talk will also discuss
ongoing extensions of this work to other high-level languages, such
as Object-Z.
Biography:(biography unavailable)
Type: ITEE Seminar
Contact:Associate Professor David Carrington, seminar host (davec@itee.uq.edu.au)
or Guido Governatori (ITEE seminar co-ordinator)
(guido@itee.uq.edu.au)