Proving Event Ordering Properties for Information Systems

摘要

This paper presents an approach to prove event ordering properties for B specifications of information systems. The properties are expressed using the EB~3 notation, where input event ordering properties are defined using a process algebra similar to CSP and output events are specified by recursive functions on the input traces associated to the process expression. By proving that the EB~3 specification is refined by the B specification, using the B theory of refinement, we ensure that both specifications accept and refuse exactly the same event traces. The proof relies on an extended labeled transition system, generated using the operational semantics of the process algebra, in order to deal with unbounded systems. The gluing invariant is generated from the EB~3 recursive functions.