A type-checker for real-time Object-Z

Abstract

Specification languages are extensively used for capturing the requirements of safety-critical and real-time applications. Most of the specification languages reported in the literature for real-time appli ations are functional; there are few object-oriented real-time specification languages such as TRIO+. Recently, Alagar and Periyasamy have extended the Object-Z specification language, an object-oriented extension of the Z specification language, towards specifying real-time constraints. This language is called Real-Time Object-Z (RTOZ). One of the problems in using formal specification languages is the lack of tool support for developing and using the specifications. Tool support for a specification language is necessary at all levels: syntax checking, type checking and semantic checking. A number of type checkers are available for Z. In addition, a few theorem provers have also been developed for Z. There is only one tool for Object-Z reported in the literature for type checking and pretty-printing. There is no tool available for RTOZ. In this thesis, a type checker for RTOZ is described. The major contributions include the development of a grammar for RTOZ and the implementation of the type checker. An interesting feature of the type checker is that it can also be used to type-check Z specifications as well as Object-Z specifications.