Sciweavers

IFM
2004
Springer

Verifying Controlled Components

14 years 5 months ago
Verifying Controlled Components
Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and controller behaviour). This approach is driven by the desire to exploit existing tool support for both CSP and B, and by the need for compositional proof techniques. This paper is concerned with the theory underpinning the approach, and proves a number of results for the development and veri cation of systems described using a combination of CSP and B. In particular, new results are obtained for the use of the hiding operator, essential for abstraction. The paper provides theorems which enable results obtained (possibly with tools) on the CSP part of the description to be lifted to the combination. Also, a better understanding of the interaction between CSP controllers and B machines in terms of non-discriminating and open behaviour on channels is introduced, and applied to the deadlock-freedom theo...
Steve Schneider, Helen Treharne
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where IFM
Authors Steve Schneider, Helen Treharne
Comments (0)