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