Abstract
CSP parallel to B is a formal approach which combines state and event-based descriptions of a system. It enables the automatic verification of dynamic properties using model checking techniques. In this paper we identify a variation on the standard CSP parallel to B architecture so that it is more applicable to support the specification of information systems. We specify a library system using this new architecture. We examine several safety and liveness requirements and demonstrate that we can compositionally verify them using FDR. If a property fails to model check we identify an abstraction technique which enables us to pinpoint the cause of the failure.