Journal
FORMAL ASPECTS OF COMPUTING
Volume 22, Issue 2, Pages 153-191Publisher
SPRINGER
DOI: 10.1007/s00165-009-0119-6
Keywords
Relational models; Unifying theories of programming; CSP; Galois connections
Categories
Funding
- Brazilian Research Council (CNPq)
- Engineering and Physical Sciences Research Council [EP/E025366/1] Funding Source: researchfish
- EPSRC [EP/E025366/1] Funding Source: UKRI
Ask authors/readers for more resources
Following the trend to combine techniques to cover several facets of the development of modern systems, an integration of Z and CSP, called Circus, has been proposed as a refinement language; its relational model, based on the unifying theories of programming (UTP), justifies refinement in the context of both Z and CSP. In this paper, we introduce Circus Time, a timed extension of Circus, and present a new UTP time theory, which we use to give semantics to Circus Time and to validate some of its laws. In addition, we provide a framework for validation of timed programs based on FDR, the CSP model-checker. In this technique, a syntactic transformation strategy is used to split a timed program into two parallel components: an untimed program that uses timer events, and a collection of timers. We show that, with the timer events, it is possible to reason about time properties in the untimed language, and so, using FDR. Soundness is established using a Galois connection between the untimed UTP theory of Circus (and CSP) and our time theory.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available