Please use this identifier to cite or link to this item:
Title: HighSpec: A tool for building and checking OZTA models
Authors: Dong, J.S. 
Hao, P. 
Zhang, X.
Qin, S.C.
Keywords: Object-Z
Structural design
Timed automata
Issue Date: 2006
Citation: Dong, J.S.,Hao, P.,Zhang, X.,Qin, S.C. (2006). HighSpec: A tool for building and checking OZTA models. Proceedings - International Conference on Software Engineering 2006 : 775-778. ScholarBank@NUS Repository.
Abstract: 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 ent as an alternative media for the spread and read of established OZTA models.
Source Title: Proceedings - International Conference on Software Engineering
ISBN: 1595933751
ISSN: 02705257
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

checked on Jun 23, 2022

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.