Abstract:Most research on test case generation from Object-Z specification focuses on theory. There is almost no tool to support generating test cases automatically. The Object-Z is a mathematics and logic based formal specification language. It uses schema composition and abbreviation format, which brings difficulty for extracting semantics and then generating test cases from specification automatically. This paper provides a solution in extracting semantics and generating test cases from Object-Z specification by unfolding the schema definition and improving its syntax in Object-Z. The process has three steps including parsing Object-Z language, extracting semantics, and generating test cases automatically.