Requirements Engineering, IEEE International Conference on (2000)
June 19, 2000 to June 23, 2000
Carl A. Gunter , University of Pennsylvania
Elsa L. Gunter , Bell Labs
Michael Jackson , AT&T Laboratories
Pamela Zave , AT&T Laboratories
We define a reference model for applying formal methods to the development of user requirements and their reduction to behavioral specification of a system. The approach is characterized by its focus on the shared phenomena that define the interface between the system and the environment in which it will operate and on how the parts of this interface are controlled. This paper extends our previous work on this model by representing it in higher-order logic and determining some of its key mathematical ramifications. In particular, we introduce a new form of refinement, which is pivotal to defining the desired soundness and consistency properties precisely.
software engineering methodology, refinement, formal methods, requirements, specifications
P. Zave, C. A. Gunter, M. Jackson and E. L. Gunter, "A Reference Model for Requirements and Specifications," Requirements Engineering, IEEE International Conference on(ICRE), Schaumburg, Illinois, 2000, pp. 189.