Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/40012
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
Verification
Issue Date: 2006
Source: 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.

Page view(s)

76
checked on Dec 9, 2017

Google ScholarTM

Check


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