Hoenicke, Jochen; Olderog, Ernst-Rüdiger CSP-OZ-DC: a combination of specification techniques for processes, data and time. (English) Zbl 1088.68643 Nord. J. Comput. 9, No. 4, 301-334 (2002). Summary: CSP-OZ-DC is a new combination of three well researched formal techniques for the specification of processes, data and time: CSP, Object-Z, and Duration Calculus. 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 for CSP and UPPAAL 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. Cited in 5 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) Keywords:CSP; Object-Z; Duration Calculus; transformational semantics; real-time processes; model-checking; FDR; UPPAAL Software:Moby/DC; Uppaal; Z/EVES PDF BibTeX XML Cite \textit{J. Hoenicke} and \textit{E.-R. Olderog}, Nord. J. Comput. 9, No. 4, 301--334 (2002; Zbl 1088.68643)