Congratulations to Beeta Vajar for successfully passing her MPhil to PhD transfer

Wednesday 19 September 2007

Abstract:

Formal methods are mathematical techniques used to specify and verify software systems. They produce precise and concise description of computer programs.

State-based formal methods, such as the B-Method, focus on data aspects of systems. On the other hand event-based formal methods, such as CSP, are concerned with behavioural aspects of the systems. Over the years, the idea of combining state and event based formal methods has been raised in order to design systems in which both data and behavioural aspects are described.

CSP || B is an approach which has been proposed in order to create a reliable, consistent and verifiable model for complex and critical systems. In this parallel combination, a CSP process is used as a control executive for a B Machine. The CSP controller is a suitable control executive if we can prove that it is consistent with its controlled B Machine. In order to prove the consistency of a CSP control executive and its controlled B Machine, we need to prove that the combined system is divergence free and deadlock free.

The systems we are generally concerned with are a collection of parallel combinations which interact with each other. These kind of systems have the form of ||i(Pi || Mi), in which each Pi is a CSP controller for B Machine Mi.

In this report, we investigate the CSP || B approach in the context of two case studies: a fire control system and a stem cell model. These expose the theoretical work required to narrow down to more practical problems with regard to this design. In addition, we present new theorems and techniques proved during this research in order to establish consistency in parallel combinations of controlled components which have not been covered before.