Linking Semantic Models to Support CSP || B Consistency Checking

Consistency checking in the CSP B approach verifies that an individual controller process, defined using a sequential non-divergent subset of CSP, never calls a B operation outside its precondition. Previously this was done by preprocessing the CSP process to perform a weakest precondition semantics proof. An embedding of the CSP traces model already exists in the PVS theorem prover, which makes use of `uniform properties' to define valid traces. By including a state model we can extend the notion of uniform properties to define consistency. In this paper we give a framework which uses these semantic embeddings to eliminate the need for preprocessing. CSP B supports compositional verification, and the added benefit of this framework is that rely/guarantee style decomposition emerges naturally during a proof of consistency. Key words: CSP, B, method integration, verification

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Neil Evans, Helen Treharne
• Keywords: ENTCS 2006, Sequential Non-divergent Subset, Uniform Properties, Weakest Precondition Semantics