CSP-OZ-DC(ID:6810/csp010)
extension of CSP-OZ to include date-specific material
Related languages
References:
Hoenicke, Jochen; Olderog, Ernst-Rüdiger "CSP-OZ-DC: a combination of specification techniques for processes, data and time", Nordic Journal of Computing, v.9 n.4, p.301-334, Winter 2002
view details
Abstract: CSP-OZ-DC is a new combination of three well researched formal techniques for the specification of processes, data and time: CSP [Hoare 1985], Object-Z [Smith 2000], and Duration Calculus [Zhou et al. 1991]. This combination is illustrated by specifying the train controller of a case study on radio controlled railway crossings. The technical contribution of the paper is a smooth integration of the underlying semantic models and its use for verifying timing properties of CSP-OZ-DC specifications. This is done by combining the model-checkers FDR [Roscoe 1994] for CSP and UPPAAL [Bengtsson et al. 1997] for timed automata with a new tool f2u that transforms FDR transition systems and certain patterns of Duration Calculus formulae into timed automata. This approach is illustrated by the example of a vending machine.
Wehrheim, Heike "Relating state-based and behaviour-oriented subtyping", Nordic Journal of Computing, v.9 n.4, p.405-435, Winter 2002 view details
|