本论文以研究和建立满足新一代网络发展需求的网络体系结构建模方法作为主要出发点，重点展开了对于面向服务的网络系统形式化描述和验证的相关研究。本文对传统网络体系结构及其形式化研究的不足进行了分析，对新形态的网络体系结构及其建模研究的成果及思路进行了总结，从而把握了网络研究和应用的重点从通信向服务进行跃迁的新趋势。 论文首先对以构件化和基于交互为主要特点的新一代网络服务体系结构INSA参考模型，及与之相应的INSA抽象形式化建模方法，进行了较为深入的介绍与分析，重点探讨了它们的优势和存在的缺陷。针对INSA形式化模型在非确定性交互等方面描述能力的不足，本文提出了一种行之有效的改进方案，即：在实体构件的实体实现逻辑单元与交互连接件的连接件胶合规则单元之中加入对各建模单元及进程间相互关系的描述，以增强它们的表示能力。论文特别注意到了在新的网络应用环境之下，无论是服务交互还是协议交互都越来越多的以多方交互的形式出现在各网络实体之间，而传统的网络协议形式化研究所主要采用的“一对一”直接交互模型已不再适用；为此在参照新一代服务体系结构形式化描述语言(通过拓展INSA参考模型、INSA形式化建模方法的研究思路及成果而建立的)INSADL的基础之上，本文分析了网络多方应用系统的建模需求，据此提出了一种对INSADL进行扩展的方案。文中介绍了对各类实体构件、交互连接件以及连接装配部分的形式化语言描述进行扩展的方法，又探讨了涉及网络多方交互的适配与相宜连接性质，以便于采用形式化方法对网络多方应用系统的性质开展进一步研究。论文为若干不同类型网络体系结构的应用实例均建立了较为详细的规约，以实际表明此前建立的形式化建模方法的描述和建模分析能力。最后从适于自动处理的角度提出了一种对INSADL的简化和改进方案，并据此实现了一种网络体系结构规约的自动解析和验证工具。 本文为面向服务的新一代网络体系结构研究提供了崭新的思路和方法，其研究结论具有一定的指导意义和参考价值。