Constructing and revising formal arguments in requirements engineering

Confidence that a proposed software-based system, once implemented, will be successful in its environment can be given through a formal argument, typically proof in a formal language. Problems with such arguments include the need to account for the relationships between different kinds of model (models of the proposed system, of assumptions concerning its environment, and of the joint properties, or requirements, which the system should achieve with its environment), and the need to revise these models within an exploratory requirements engineering process. This paper investigates the assumption/commitment style of modelling, originally developed for reasoning about interference in concurrent systems, for developing such arguments. The style, using a simple temporal logic, is used to express these models, with an associated compositional reasoning method allowing arguments to be constructed, and revised with minimal re-work of proof. Some conclusions are drawn concerning the benefits of, and problems with, this approach. The approach is illustrated with a meeting-scheduler example.