基于SPIN的功能测试用例生成方法研究

提出了一种自动生成系统功能测试用例的新方法。该方法使用Promela语言对软件系统的状态和行为进行描述建模，使用LTL公式描述测试覆盖标准，然后将该组LTL公式和描述状态行为的Promela模型输入SPIN模型检测工具，并利用模型检测工具自动生成相应的证据路径，最后结合正例将路径转化成满足相应覆盖标准的系统功能测试用例，并以电梯系统模型对该方法作出了诠释。