How to verify dynamic properties of information systems

EB³ is an established formal technique, based on process algebra, for specifying Information Systems (IS) that have both complex state and event based features; as yet, EB³ has no tool support. Another formal technique called CSP || B uses two existing analysis tools, FDR and the B-Toolkit, to support the verification of state/event based systems. However the CSP || B approach has never been applied to this specialised domain. In this paper we use a specification pattern of EB³ to motivate a new style of specification in CSP || B appropriate for IS. We demonstrate this using an example system and show that the verification of its dynamic properties is now amenable to tool support.