Actualmente, las empresas enfrentan el desafío de la personalización de la producción, caracterizada por lotes pequeños de una variedad de productos. Esto adiciona un problema a la ya compleja planeación y control de la producción (PPC). En la industria de procesos el estándar ISA-88 proporciona modelos para definir los requisitos de control para las plantas de fabricación por lotes. La implementación de Gemelos Digitales (GD) basados en AAS (Asset Administration Shell) puede soportar la automatización de la toma de decisiones en la PPC. La plataforma I4.0 propone un metamodelo para especificar la información de un AAS mediante submodelos basados en estándares que representen las diversas vistas de un activo. En particular, en la industria de procesos no se encontraron submodelos que permitan la definición de AAS. Con el fin de definir un AAS para la construcción de GD en este tipo de industrias, se está trabajando en la definición de submodelos basados en el estándar ISA-88. En particular, este trabajo presenta la formalización del lenguaje grafico conocido como SFC (Sequential Function Chart) como base para la definición del submodelo que representa la parte procedural de una receta ISA-88. La definición del submodelo se realizó utilizando el Lenguaje Unificado de Modelado (UML) y OCL (Object Constraint Languaje) para formalizar las restricciones. Contar con la formalización de un lenguaje gráfico permite la verificación de la construcción de modelos válidos, mediante la detección de redes inseguras e inalcanzables. Si bien surge de la necesidad de la representación formal de la parte estructural de una receta y su uso en un GD de la industria de procesos batch, puede ser utilizado en cualquier tipo de industria dado que el mismo es una de las alternativas propuestas por el estándar IEC 61131-3 para la automatización industrial.