Towards automated tool support for RTOZ: Decidability of TIC
Speaker: Geoff Kassel, ITEE
When: 2003-05-13 14:00:00
Venue: 78-420
Host: Dr Graeme Smith
Abstract:Real Time Object-Z (RTOZ) is a recent real-time specification
language merging two distinct set-theoretical formalisms, Object-Z
and the Timed Interval Calculus (TIC). These provide RTOZ with the
specification power of object orientation in a temporal domain.
Tool support improves the industrial applicability of formal
methodologies, most notably so when the process is in any part
automated. The ability to evaluate the truth of any given statement
in a language - its decidability - is crucial for use with the
automated reasoning needed for automated tool support. Determining
the decidability of a language is hence a common first step towards
development of such a capability.
Automated reasoning is not yet a reality for the composite
formalisms of RTOZ. However, of these languages, TIC is most open to
the determination of decidability. This is due to its compactness
syntactically and semantically, and its similarity to other
languages with known decidability results.
This PhD confirmation seminar discusses the topic of decidability of
TIC. Decidability results will be discussed within the framework of
the larger topic of developing automated tool support for RTOZ.
Biography:(biography unavailable)
Type: Ph.D confirmation
Contact:Dr Graeme Smith, seminar host (smith@svrc.uq.edu.au)
or Guido Governatori (ITEE seminar co-ordinator)
(guido@itee.uq.edu.au)