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.
|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||URI:||http://scholarbank.nus.edu.sg/handle/10635/40012||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.
checked on Oct 28, 2019
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.