Specification and Verification of Reactive Systems with RSDS

Abstract

Formal methods have been applied to reactive systems in order to capture errors early on in
the development life-cycle and reduce redesign costs. The Reactive Systems Development Support
(RSDS) method provides support for the analysis and design of reactive systems and generates code
from these specifications. An RSDS system is specified by a set of invariants, a set of statemachines
and a Data Control Flow Diagram (DCFD), which are then verified using the B theorem-prover.
B however requires user interaction and is not capable of proving temporal properties easily. This
thesis extends RSDS by integrating model checking so that temporal properties can be verified.
The model checker used is the Symbolic Model Verifier (SMV).
There are two distinct semantic views of statemachines in RSDS: the coarse-grain and the
fine-grain, with the key difference between them being the granularity of a step. We describe a
translation to SMV for each semantic view and we guarantee the quality of the translations by
formally proving their correctness. This proof is a vital part in our provision of transparent formal
method support for system design. To overcome the state explosion problem of model checking, we
propose some natural ways of using the RSDS decomposition techniques for dividing the system
into subsystems; these can then be model checked independently as separate SMV programs. We
have tested our translations with various case studies.
RSDS/UML is an object-oriented version of RSDS that uses a restricted subset of UML for
specification. It aims to bridge the gap between formal methods and mainstream software development
techniques. For the same reasons as with RSDS, we integrate model checking with
RSDS/UML by defining a translation for the coarse-grain and proving its correctness. The properties
verified can reason over the dynamic instantiation of classes. The translation is illustrated
on the gas burner system.

Date of Award	1 Jun 2004
Original language	English
Awarding Institution	King's College London
Supervisor	Kevin Lano (Supervisor)