J.S. Dong
HighSpec: a Tool for Building and Checking OZTA Models
Dong, J.S.; Hao, P.; Zhang, X.; Qin, S.
Authors
P. Hao
X. Zhang
S. Qin
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 document as an alternative media for the spread and read of established OZTA models.
Citation
Dong, J., Hao, P., Zhang, X., & Qin, S. (2006). HighSpec: a Tool for Building and Checking OZTA Models. In 28th International Conference on Software Engineering, 20-28 May 2006, Shanghai, China ; proceedings (775-778). https://doi.org/10.1145/1134409
Conference Name | 28th International Conference on Software Engineering (ICSE 2006) |
---|---|
Conference Location | Shanghai, China |
Start Date | May 20, 2006 |
End Date | May 28, 2006 |
Publication Date | May 1, 2006 |
Deposit Date | Nov 16, 2009 |
Publisher | Association for Computing Machinery (ACM) |
Pages | 775-778 |
Book Title | 28th International Conference on Software Engineering, 20-28 May 2006, Shanghai, China ; proceedings. |
DOI | https://doi.org/10.1145/1134409 |
Keywords | Object-Z, Structural design, Timed automata, Verification. |
Publisher URL | http://doi.acm.org/10.1145/1134409 |
You might also like
PTSC: probability, time and shared-variable concurrency
(2009)
Journal Article
Memory Usage Verification Using Hip/Sleek
(2009)
Conference Proceeding
An Interval-based Inference of Variant Parametric Types
(2009)
Conference Proceeding
A Heap Model for Java Bytecode to Support Separation Logic
(2008)
Conference Proceeding
Downloadable Citations
About Durham Research Online (DRO)
Administrator e-mail: dro.admin@durham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search