rΣ: Automated reasoning tool for non-functional requirement goal models

Reasoning is critical for non-functional requirements (NFRs) analysis and verification. Furthermore, it can provide rationale about implementation strategies for NFRs. The existing tools can execute an interactive reasoning process which sometimes needs extra information from stakeholders. We build a tool called rΣ for reasoning on NFR models especially when extra information is unavailable or forbidden, like at the model verification stage. This tool employs the formula style model as the input, automatically promotes the reasoning process till the root node, and returns all the satisficing statuses and the complete rationale as the output. We have applied rΣ into the real practice and to evaluate its efficiency.