Please use this identifier to cite or link to this item: https://scholarbank.nus.edu.sg/handle/10635/40012
DC FieldValue
dc.titleHighSpec: A tool for building and checking OZTA models
dc.contributor.authorDong, J.S.
dc.contributor.authorHao, P.
dc.contributor.authorZhang, X.
dc.contributor.authorQin, S.C.
dc.date.accessioned2013-07-04T07:54:41Z
dc.date.available2013-07-04T07:54:41Z
dc.date.issued2006
dc.identifier.citationDong, 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.
dc.identifier.isbn1595933751
dc.identifier.issn02705257
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/40012
dc.description.abstractHighSpec 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.
dc.sourceScopus
dc.subjectObject-Z
dc.subjectStructural design
dc.subjectTimed automata
dc.subjectVerification
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.sourcetitleProceedings - International Conference on Software Engineering
dc.description.volume2006
dc.description.page775-778
dc.description.codenPCSED
dc.identifier.isiutNOT_IN_WOS
Appears in Collections:Staff Publications

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

Google ScholarTM

Check

Altmetric


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