Verifying the Relationship Among Three Descriptions in Problem Frames Using CSP

In requirements engineering (RE), there are three essential descriptions, i.e., requirements, specification and domain properties. Their relationship is proposed by Jackson et al, and verified in various requirements approaches. However, at present, there is no formal verification for the relationship in the Problem Frames (PF) which is a well known approach in the RE. Our previous work based on the PF explicitly captures the three descriptions. Based on that work, this paper further formalizes the three descriptions using Communicating Sequential Process (CSP), transforms the relationship into two "refines", and verifies them with Process Analysis Tool (PAT). The verification ensures that the machine which behaves as in the specification installed in a specific domain will satisfy the requirements.