摘要： 传统方法中基于软件测试工程师经验的测试用例构造技术使得软件测试的质量很难得到保证。本文提出一种基于形式化方法的软件测试模型。该模型使用形式化描述语言RSL对软件设计进行描述，并在此基础上提出了自动生成软件测试各个阶段所需测试用例的方法框架以及相关实验结论。

关键词: 软件测试模型 测试用例 形式化方法 描述语言 RSL 自动生成 软件设计 实验结论 阶段 传统方法