[8-19]Tools for CSP
Date:2010-08-18
Title: Tools for CSP
Speaker: Markus Roggenbach
Time: 3:00pm, Thursday August 19, 2010
Venue: Lecture Room, Level 3, State Key Lab. of Computer Science
Abstract:
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. The claim is: Eventually, all children will hold the same number of candies."
Taking the above described "Children & Candy Puzzle" as a starting point, we discuss how to model it in the process algebra CSP and how to prove its claim using standard CSP tools for simulation (ProBe), model checking (FDR), and theorem proving (CSP-Prover). Besides the power to analyze a single system, 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.
Short bio. of the speaker:
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 Karlsruhe, did his PhD in Mannheim, and worked as a postdoc in Bremen. In Swansea, he built up an active research group with currently four doctoral students.
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 main contributions include the semantical foundations and design of the specification languages CoCASL and CSP-CASL; 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.