Este anexo F1 establece la motivación, describe la estructura general de la semántica formal y contiene una introducción a la máquina de estados abstractos (ASM, abstract state machine), formalismo que es usado para definir la semántica SDL.