Combining Specification Techniques for Processes, Data and Time

Abstract. We present a new combination CSP-OZ-DC of three well researched formal techniques for the specification of processes, data and time: CSP [17], Object-Z [36], and Duration Calculus [40]. The emphasis is on a smooth integration of the underlying semantic models and its use for verifying properties of CSP-OZ-DC specifications by a combined application of the model-checkers FDR [29] for CSP and UPPAAL [1] for Timed Automata. This approach is applied to part of a case study on radio controlled railway crossings.

• Type: Conference
• Year: 1998
• Where: ZUM
• Authors: Ernst-Rüdiger Olderog
• Keywords: Duration Calculus, Formal Methods, Formal Techniques, Radio Controlled Railway, ZUM 1998