Sciweavers

ENTCS
2006

Linking Semantic Models to Support CSP || B Consistency Checking

13 years 12 months ago
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
Neil Evans, Helen Treharne
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Neil Evans, Helen Treharne
Comments (0)