本文研究的重点是SDL的形式语义定义方法，在分析SDL-88和SDL-2000语义定义方法的基础上提一种改进的SDL-2000形式语义的方法。另一方面，考虑到SDL与UML结合使用的发展趋势，提出用ASM定义UML形式语义的思想，使SDL和UML可以在语义级统一起来。此外，本文对形式验证SDL规范的相关问题作了初步探讨，以期扩展SDL形式语义定义的应用。 针对SDL静态语义，本文提出的方法将语法域中元素视为项，SDL规范的所有子项可以表示为作用于该SDL规范的函数形式。从这个角度看，良形式条件定义了SDL规范及其子项之间的约束关系；转换规则定义了用基本概念子项替换SDL规范中补充概念子项的模型；映射规则定义了从AS0的语法域到AS1的语法域的对应关系。其中，转换规则直接采用ASM的更新规则定义局部SDL规范的更新；映射规则应用一系列t-函数实现，从而不必引入重写规则或使用嵌套模式。 针对SDL动态语义，本文提出的方法采用解释执行的方式通过跟踪具有执行权的agent实例的当前状态及其关联的动作序列，解释执行动作序列中的动作。这样，SDL规范与其ASM语义模型可以直接关联起来，从而提高了语义定义的连贯性和可理解性。对于复杂的动作，可以通过引入辅助动作来帮助描述复杂动作的细节。对于面向对象的语法概念，可以通过特定函数计算或构造完整的展开定义。此外，这种方法将系统实例创建为实例结构树的形式，可以简化处理过程调用和选择异常处理器时保存和恢复控制信息的问题；信号流模型可以从gate的角度定义。这种动态语义定义方法可以采用基本ASM来描述以便于形式验证(如ModelChecking)的需要。 UML的出现和普及对SDL语言在面向对象方面的发展产生了深远影响。建议Z.109专门制定了从UML到SDL的映射规范。为了放宽对SDL与UML结合使用的约束，采用相同的元语言定义动态语义可以促进SDL与UML一致地结合使用。考虑到ITU-T已采用ASM定义SDL的形式语义，因此，采用ASM定义UML的形式语义可以使SDL和UML在语义级一致地表示为ASM模型。考虑到UML的复杂性，本文主要给出了定义UML状态机动态语义的方法框架，与现有的其它方法相比，这种语义定义可以反映UML状态机的全部语义特征。 由于基本ASM模型可以视为基于ASM理论的可执行规范语言AsmL的伪代码，ASM语义模型可以方便地转换为相应的AsmL程序。这样，利用AsmL集成环境提供的从AsmL程序生成状态变迁图的功能，本文给出通过ASM语义模型采用ModelChecking验证SDL规范的方法框架。此外，考虑到用于ModelChecking的时序逻辑公式过于数学化，本文给出用直观明了的路径模式法来表示系统特性以及采用这种表示法构造Büchi自动机的方法。