Deep Semantic Links of TCSP and Object-Z: TCOZ Approach
- 1 May 2002
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 13 (2) , 142-160
- https://doi.org/10.1007/s001650200004
Abstract
: Formal methods can be used in effective combination only if the semantic links between individual methods are clearly established. This paper discusses the semantic design of TCOZ, a language blended from Object-Z and TCSP. The semantic model adopted is the infinite timed failures model of TCSP, extended to include initial state and update events for modelling operations on internal state. An infinite trace model has been used so as to ensure proper account is taken of the potentially unbounded non-determinism allowed by Z schemas.Keywords
This publication has 6 references indexed in Scilit:
- Blending Object-Z and Timed CSP: an introduction to TCOZPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSPFormal Methods in System Design, 2001
- The Object-Z Specification LanguagePublished by Springer Nature ,2000
- A fully abstract semantics of classes for Object-ZFormal Aspects of Computing, 1995
- Fixed points without completenessTheoretical Computer Science, 1995
- A timed model for communicating sequential processesTheoretical Computer Science, 1988