随着互联网技术的广泛普及和飞速发展,高清视频、实时会议和在线点播等新型网络应用的不断出现,骨干网流量呈爆炸式增长,这对底层网络部署业务的灵活性和稳定性提出了挑战。弹性光网络(Elastic Optical Network,EON)采用灵活的频谱划分、动态的光路管理机制和先进的碎片整理技术,这使其成为解决光网络频谱资源紧缺问题的重要方案。本文依托国家自然科学基金项目“混合弹性光网络中资源优化的新型智能算法及形式化”,完成EON中资源优化问题的形式化模型的构建以及智能优化算法的形式化与验证两部分工作。国内外大量研究集中于EON中的不同场景,侧重于具体问题的求解,在宏观上缺少对EON资源分配问题中业务源、网络拓扑、智能算法和数学约束等组件的形式化描述,难以形成统一的严格一致的知识库。形式化理论基于严格的数学基础,为系统分析提供一致性的规范、建模和验证方法。本文着重从形式化研究的角度,构建EON中的资源分配问题及其求解算法的形式化模型,建立相应知识的一致性描述,为算法改进提出创新的分析方法,并为网络资源分配软件的开发提供一致的框架雏形,主要内容和创新点包括以下三个方面:形式化方法已经广泛应用在通信协议验证、知识处理、硬件制造和软件工程等多个领域,关键系统的建模和可靠性分析离不开形式化理论。本文从资源分配角度概述了形式化方法的发展和应用,说明了形式化建模的重要性和必要性。横向对比了不同的形式化方法的特点和属性,选用着色Petri网(Colored Petri Nets,CPN)作为建模理论,并总结了现有Petri网仿真工具的优缺点。尽管已有研究涉及将形式化方法应用到光网络的资源及组件属性的描述,以及相关智能优化算法的建模中,但所构建模型没有体现EON资源分配的约束和特性。为解决EON中的静态路由与频谱分配(Routing and Spectrum Allocation,RSA)问题,本文采用CPN实现了RSA数学模型向形式化模型的转换,通过各个关键模块的正确性检查以及模型的动态性质分析,验证了所构建CPN模型的一致性,为深化RSA的认识提供了理论依据。通常智能算法被用于解决静态RSA问题以优化目标函数,遗传算法是相关研究中应用最广泛的一类元启发式算法。本文根据适应度值分布特点来计算更适合当前进化状态的参数,设计了三个遗传算子的自适应策略。利用CPN对遗传算法的染色体编码、适应度值计算和遗传操作等其他算法模块进行形式化建模,对提出的选择、交叉和变异的自适应算子模型的流程进行详细分析,完成了解决RSA优化问题的遗传算法的形式化描述。同时,本文利用CPN Tools对模型进行仿真,仿真结果验证了所提自适应策略的有效性以及各个功能模块的正确性,确保形式化模型的一致性。通过分析模型运行过程中库所与迁移的动态属性,为利用知识管理方法来改进算法关键要素提供了不同于传统方法的途径。