A formal definition of FRSM and applications

FRSM (Formal Requirements Specification Method) is a structured formal language and method for requirements analysis and specification construction based on data flow analysis. It uses a formalized DeMarco data flow diagram to describe the overall structure of systems and a VDM-SL like formal notation to describe precisely the functionality of components in the diagrams. This paper first describes the formal syntax and semantics of FRSM and then presents an example of using the axiom and inference rules given in the definition of the formal semantics for checking consistency of specifications. A case study of applying FRSM to a practical example is described to demonstrate the principle of constructing requirements specifications and to uncover the benefits and deficiencies of FRSM.