When Michael Jackson and I began to work on formal methods for requirements engineering, we were puzzled by many aspects of basic issues such as control, the problem of implementation bias, and the meaning of requirements refinement. We felt that we could not write meaningful specifications until we understood these issues better.
Starting with Michael's ideas on these issues, developed over many years of rumination on software development, we wrote "Domain descriptions" (Michael Jackson and Pamela Zave; IEEE International Symposium on Requirements Engineering, pages 56-64, IEEE Computer Society Press, 1992). In 2003 this won the International Requirements Engineering Symposium Ten-Year Most Influential Paper Award.
Eventually the work matured to the framework for requirements engineering described in "Four dark corners of requirements engineering" (Pamela Zave and Michael Jackson; ACM Transactions on Software Engineering and Methodology VI(1):1-30, January 1997).
This paper shows that, when it comes to requirements, the environment is not the most important thing--it is the only thing. It explains the precise nature of requirements, specifications, and domain knowledge, as well as the precise nature of the relationships among them. The framework establishes minimum standards for what information should be represented in a requirements language. The framework also makes it possible to determine exactly what it means for requirements engineering to be successfully completed.
"Four dark corners of requirements engineering" has many small, fragmentary examples. For a complete example of this way of looking at requirements, see "Deriving specifications from requirements: An example", (Michael Jackson and Pamela Zave; 17th International Conference on Software Engineering, pages 15-24, ACM Press, 1995). In 2005, this won the International Conference on Software Engineering Ten-Year Most Influential Paper Award.
Another complete example can be found in "The village telephone system: A case study in formal software engineering" (Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, and Pamela Zave; 11th International Conference on Theorem Proving in Higher Order Logics, LNCS 1479, 1998).
Finally, this material was condensed and published as "A reference model for requirements and specifications" (Carl A. Gunter, Elsa Gunter, Michael Jackson, and Pamela Zave; IEEE Software XVII(3):37-43, May/June 2000). The first version of this paper was presented at the IEEE International Conference on Requirements Engineering in 2000, and in 2010 it won the conference's Ten-Year Most Influential Paper Award.
Out of my role as program chair of the 2nd IEEE International Symposium on Requirements Engineering came "Classification of research efforts in requirements engineering" (Pamela Zave; ACM Computing Surveys XXIX(4):315-321, December 1997). The classification scheme described in it was used to organize the second and third symposia of this series.