×

zbMATH — the first resource for mathematics

Deep semantic links of TCSP and Object-Z: TCOZ approach. (English) Zbl 1063.68603
Summary: 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.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
Software:
TCOZ
PDF BibTeX XML Cite
Full Text: DOI