本成果旨在解决开发中SDN应用的安全属性测试难题，提出了一种创新的测试方法。该方法通过构建与开发中SDN应用功能说明相适应的形式化模型及安全约束，利用模型检测工具探索模型状态空间，生成测试脚本，并对原型实现进行迭代测试。通过不断发现并修复潜在的安全漏洞，确保最终版本的功能说明、安全属性和原型实现均满足安全要求。 核心技术： （1）形式化建模与安全约束：根据开发中软件定义网络（SDN）应用的功能说明，构建形式化模型，该模型包含描述SDN应用实体的进程、通信链路的信道和应用数据的数据结构。同时，根据提取的安全属性（如网络安全规则和功能），制定与安全属性相适应的安全约束。 （2）模型检测与反例生成：利用模型检测工具探索形式化模型的状态空间，检测是否存在违反安全约束的情况。一旦发现违反，模型检测工具将生成反例，反例包含进程列表、消息序列等关键信息。 （3）测试脚本自动生成：基于生成的反例，自动解析反例中的进程列表与消息序列，生成相应的测试脚本。测试脚本中设置测试判决条件，用于验证SDN应用原型实现的正确性。 （4）原型实现迭代测试：使用生成的测试脚本对SDN应用的原型实现进行测试，根据测试结果修改功能说明和原型实现。通过多轮测试-修正-再测试的迭代过程，不断优化SDN应用的安全性和准确性。 （1）迭代测试支持：首次提出针对开发中的SDN应用原型实现进行迭代测试的方法，填补了现有测试方法在开发阶段应用的空白。 形式化建模与约束：构建精确的形式化模型和安全约束，确保测试的全面性和准确性。 （2）自动化测试脚本生成：根据模型检测工具生成的反例，自动生成测试脚本，提高测试效率。 （3）全流程测试覆盖：通过多轮测试-修正-再测试的迭代过程，确保最终版本的稳定性和安全性。 （4）高度灵活性与可扩展性：支持不同版本的SDN应用测试，可适应不同的开发环境和需求。