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. |
|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|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 8, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.