Tools for CSP - Overview and Perspectives
- When?
- Wednesday 15 June 2011, 14:00 to 15:00
- Where?
- 39BB02
- Open to:
- Staff, Students
- Speaker:
- Dr Markus Roggenbach, Swansea University
Our speaker will be Dr Markus Roggenbach, from the Department of Computer Science, Swansea University.
Taking the "Children & Candy Puzzle" (see below) as a master example, we discuss what the various tools for the process algebra CSP offer for modelling and verifying systems. Here, we focus especially on interactive theorem proving for CSP, as exemplified in Steve Schneider's work or in our tool CSP-Prover. Besides the power to analyze infinite state systems, the theorem proving approach offers the possibility for deeper reflections on CSP. Here we discuss how it allows one to verify the algebraic laws of the language, and, furthermore, how it allows to prove meta results such as the completeness of axiomatic semantics.
Children & Candy Puzzle: "There are k children sitting in a circle. In the beginning, each child holds an even number of candies. The following step is repeated indefinitely: Every child passes half of her candies to the child on her left; any child who is left with an odd number of candies is given another candy from the teacher. Claim: Eventually, all children will hold the same number of candies."
Markus Roggenbach is a senior lecturer of Computer Science in the School of Physical Sciences at Swansea University, Wales, United Kingdom. He studied Computer Science in Braunschweig and Karlsruhe, did his PhD in Mannheim, and worked as a postdoc in Bremen. In Swansea, he built up an active research group on the topic of "Processes and Data".
His research activities concern the modelling, verification, and validation of distributed systems with a special focus on the interplay between processes and data. He is a member of the IFIP WG 1.3. "Foundations of System Specification". His contributions include the semantical foundations and design of the specification languages CoCASL and CSP-CASL; the development and implementation of a consistency calculus for structured specifications; theorem proving for process algebra; completeness of axiomatic CSP semantics; industrial case studies on formal methods
