Incremental requirements specification withLotos

The importance of formally and incrementally specifying requirements is discussed. An approach based on LOTOS (Language Of Temporal Ordering Specification) is proposed that exploits desirable characteristics of the constraint-oriented style. The nature of constraint-oriented specification is discussed at some length, and guidelines for how to use it effectively with LOTOS are presented. Small introductory examples lead to the incremental specification of a file access system using the approach in the paper. It is shown how the requirements for the file access system can be gradually formalised, leading to a complete system specification.