HighSpec: A tool for building and checking OZTA models

Jin Song Dong, Ping Hao, Xiao-Yang Zhang, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

119 Downloads (Pure)


HighSpec is an interactive system for composing and checking OZTA specications. The integrated high level specication language, OZTA, is a combination of Object-Z (OZ) and Timed Automata (TA). Building on the strength of Object-
Z's in specifying data structures and Timed Automata's in modelling dynamic and real-time behaviors, OZTA is well suited for presenting complete and coherent requirement models for complex real-time systems. HighSpec supports editing, type-checking as well as projecting OZTA models into TA models and Alloy Models so that TA model checkers-UPPAAL and the Alloy Analyzer can be utilized for verication. Most importantly, HighSpec supports a novel yet evective mechanism advocated by OZTA for structural TA design, i.e., using a set of composable timed patterns to capture high level timing requirements and process behaviors and generate the TA part of model in a top-down way. HighSpec can also generate LATEX document as an alternative media for the spread and read of established OZTA models.
Original languageEnglish
Title of host publicationProceedings of the 28th international conference on software engineering
Publication statusPublished - 2006
Event28th International Conference on Software Engineering - Shanghai, China
Duration: 20 May 200628 May 2006
Conference number: 28


Conference28th International Conference on Software Engineering

Bibliographical note

ACM allows authors' version of their own ACM-copyrighted work on their personal servers or on servers belonging to their employers.


Dive into the research topics of 'HighSpec: A tool for building and checking OZTA models'. Together they form a unique fingerprint.

Cite this