Applying CSP || B to information systems.

CSP || 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 || 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. [ABSTRACT FROM AUTHOR]