Using formal methods for requirements specification of a proposed POSIX standard

Demonstrates the utility of formal methods in the development of requirements for standards. We describe the results of an exercise to generate a formal specification of the forthcoming POSIX P1003.21 standard on real-time distributed systems communications. This exercise was conducted by a relative novice in formal methods who did not have significant POSIX domain knowledge. With the assistance of both formal methods experts and domain specialists, the formal specification activity raised a number of issues early in the evolution of the standard. Resolution of these issues by the domain specialists will lead to an improved standard, whether or nor the formal specification is included in the standard. In this paper, we present a classification and analysis of the types of issues raised using our formal approach. Our experience establishes more clearly the benefits of a formal approach to requirements engineering