Abstract: Formal methods are used to provide formal and systematic models that can be used in software development to improve the correctness in those models. Formal methods are crucial, particularly, in critical systems where even minor mistakes can be pricey. In this paper, a formal method tool: ZEVES is used to describe requirements for two systems formally. Formal requirements are then used as an input for a tool used to automatically generate, execute and verify test cases. Path coverage algorithms are used to evaluate the effectiveness of the generated test cases and the ability of the formal model to describe all or most of the system functional requirements.