中文摘要：

对测试驱动开发中测试用例的自动生成和管理问题进行了研究，并对现有方法进行了分析和比较。给出了一种基于形式化方法的测试用例生成和管理方案。该方案通过形式化语言描述软件规约，并通过相应工具生成和管理测试用例，从而提高了测试驱动开发的效率。最后给出了该方案在极限编程各个开发阶段的应用。

英文摘要：

Test case automatic generation and management in Test-Driven development are studied, and the existing solutions to which are compared. A solution based on formal method to generate and manage test cases is put forward. Through formal language describing software contract and corresponding tools generating and managing test cases, this solution can improve the efficiency of Test-Driven development. Finally, this solution＇s application in some steps of Extreme Programming is given.