A type-checker for real-time Object-Z
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...
| Main Author: | |
|---|---|
| Format: | Others |
| Language: | en en_US |
| Published: |
2007
|
| Online Access: | http://hdl.handle.net/1993/870 |
| Summary: | 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. |
|---|