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:||http://dx.doi.org/10.1145/1134409|
|Record Created:||16 Nov 2009 16:50|
|Last Modified:||30 Jul 2010 12:21|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|