FAUST: formal analysis using specification tools

Developing high quality requirements specifications is a necessity for a number of critical industrial systems. An integrated toolset, called FAUST, is proposed to assist in the production of such specifications based on the KAOS goal-driven methodology. The tool suite is designed to naturally extend the existing semiformal modeling framework and to allow formalizing only the relevant critical parts. Two tools from the toolset are presented. The requirements checker performs KAOS goal-level checks using existing model checking technology. The requirements animator produces domain-level animations hiding formality even further.