This talk will discuss the issue of responsiveness of interoperating components: one not causing the other to deadlock. In CSP process algebra terms, responsiveness can be captured for deadlock-free processes by simply requiring their parallel composition to be deadlock-free. However, the issue becomes more subtle when dealing with processes which can non-deterministically block, either through graceful termination or unfortunate deadlock. Our contribution is to define appropriate properties which can be mechanically checked, and to demonstrate the suitability of these properties as a characterization of responsiveness. Our formulation is relational. Relational properties are not in general preserved by refinement, but significantly, our formulation is refinement-closed. Model-checking is provided by the FDR tool. This is joint work with Jane Sinclair.

For more information about the Penn Logic and Computation Seminar, please see the seminar web page.