Name:
Kirsten Winter
Affiliation:
Software Verification Research Centre
Email Address:
kirsten@svrc.uq.edu.au
Location:
room 404, bld GP South (Bldg No. 78)
Phone:
3365 1638
URL:
http://www.svrc.it.uq.edu.au/pages/Kirsten_Winter.html
Research Interests:
Formal Methods, Model Checking, automated proof techniques

Project Title:
Model Checking of Object-Z
Keywords:
Object-Z, Model Checking, SMV
Units:
#8
Availability:
Prerequisites:
Knowledge and interest in formal specification (especially Object-Z). Interest in formal verification (especially model checking).
Joint supervisor:
Dr. Graeme Smith
Description:
Model Checking is an approach to the automated analysis of
formal specifications. The aim of this project is to extend
the capability of model checking to the high-level specification
language Object-Z.
Previous attempts have either been inefficient or based only on a
subset of the Object-Z language. These experiences, however,
have led to a new idea for the interface from Object-Z to the
model checker SMV.
The task of the project will be to develop a transformation
schema based on this idea that would allow Object-Z to be
transformed into SMV code. The correctness of this code
will be determined by checking properties with the SMV tool.
Template Last Revised: 14 December 2001
Template Author: Anthony MacDonald

On This Site