基于Z规格说明的软件测试用例自动生成

提出了一种基于Ｚ规格说明的软件测试用例自动生成方法，通过对软件Ｚ规格说明的分析，找出描述软件输入、输出约束的线性谓词，经过线性谓词转换， 线性谓词到线性不等式组的转换，找出区域边界顶点和边界附近的测试点等过程自动生成测试用例．同时还介绍了基于Ｚ规格说明的软件测试用例自动生成方法的实现，