CSP||B (pronounced CSP parallel B) is an approach that combines a state and event based approach to describing complex systems. The approach establishes the principles of combining the B-Method and the process algebra CSP. The B-Method is a mathematically rigorous method for the specification, design and implementation of software components. CSP is a specification language and formal notation for describing concurrency behaviour in systems.
The development of the CSP||B approach began in 2000, and is motivated by the desire to use the best of both state-based development and event level analysis. A number of theoretical results have been established which identify conditions for combining B and CSP descriptions in a consistent way, and for compositional analysis, verification and development.
The most important driver for the approach is that we use established industrial tools: FDR (by Formal Systems) and ProB (by FormalMind). ProB has a direct facility for simulating CSP||B models.
The CSP||B group is based at the University of Surrey, but we are always interested in developing new research collaborations with others. For example, in collaboration with the University of Paderborn, Germany we are continuing to develop its theoretical foundations. With the University of Swansea, Wales we are applying CSP||B to the railway domain, and this is an exciting area of development for because it is bringing forth the challenges of Timed CSP.
This website gives a flavour of what CSP||B is about but we always welcome any queries.