We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

HighSpec : a tool for building and checking OZTA models.

Dong, J. S. and Hao, P. and Zhang, X. and Qin, S. (2006) 'HighSpec : a tool for building and checking OZTA models.', in 28th International Conference on Software Engineering, 20-28 May 2006, Shanghai, China ; proceedings. , pp. 775-778.


HighSpec is an interactive system for composing and checking OZTA specifications. The integrated high level specification 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 verification. Most importantly, HighSpec supports a novel yet effective 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.

Item Type:Book chapter
Keywords:Object-Z, Structural design, Timed automata, Verification.
Full text:Full text not available from this repository.
Publisher Web site:
Record Created:16 Nov 2009 16:50
Last Modified:30 Jul 2010 12:21

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Look up in GoogleScholar | Find in a UK Library