列车自动防护(Automatic Train Protection,ATP)是列控系统的核心,负责监控列车速度,防止列车超速,是典型的安全苛求系统。作为安全苛求系统,对车载ATP进行严格的测试是十分必要的。形式化方法是一种提高软件系统,特别是安全苛求系统的安全性与可靠性的重要手段。SCADE(Safety Critical Application Development Environment)是一种基于模型的开发方法,这种方法目前已经被广泛的应用于轨道交通信号领域。目前在SCADE方面的研究集中于基于模型的开发方法,对基于SCADE的软件测试方法鲜有研究。针对车载ATP软件传统测试方法中测试用例依靠人工编写且质量难以保证的问题,提出了一种基于SCADE模型的车载ATP软件测试方法。论文主要研究内容包括以下方面:(1)建立了用于测试的车载ATP功能模型。利用SCADE中的数据流图和安全状态机,建立了车载ATP的模式转换模型和速度监控模型。形式化的建模方法不仅保证了由模型到代码的正确性,同时也确保了测试中模型与被测系统的一致性。(2)提出了一种基于SCADE安全状态机模型的状态迁移路径生成的方法。首先将状态机模型转换为路径迁移图,然后利用搜索算法,根据全迁移覆盖准则,从路径迁移图中选择状态迁移路径。该方法生成的状态迁移路径实现了对安全状态机的全状态及全迁移覆盖。(3)提出了一种由状态迁移路径得到测试数据,并生成测试用例的方法。首先根据修正条件判定覆盖准则及划分等价类方法,从状态迁移路径中得到满足迁移条件的测试数据,然后将测试数据集与状态迁移路径结合,得到测试用例。采用测试用例在SCADE环境中对车载ATP模型进行测试,修正条件判定覆盖率平均值为80.1%。(4)开发了一套测试用例自动生成工具。基于本文提出的方法,在C#环境下设计实现了一套测试用例自动生成工具。实现了对SCADE模型文件的解析与测试用例自动生成,生成的测试用例可直接用于SCADE模型测试。本文的研究结果表明,本文提出的基于SCADE安全状态机模型的测试用例生成方法,生成的测试用例满足全迁移覆盖,且可以直接用于SCADE开发的软件测试中。