When applying requirements engineering in a project work flow requirement analyses represents one of the major corner stones. Each requirement and the set of all requirements, which builds the specification, needs to be evaluated in order to reveal possible imperfections. Requirements must not lead to a contradicition or be redundant when added to the set of existing requirements. A measure of completeness for the specification needs to be defined and applied. It is also possible to generate oracles to predict the output of test cases applied to the system or the test model by formalizing the requirements. To achieve the functionality stated above we aim to introduce methods learned from the formal verification of hardware systems into requirements analysis.