Reduciendo la ambigüedad en el modelo del dominio mediante especificaciones formales ligeras en VDM++

Abstract

Una de las herramientas más utilizadas para modelar los requerimientos funcionales es el Modelo del Dominio. Muchas veces, dependiendo de la complejidad de los requerimientos a ser modelados, no es posible que dicho modelo capture todos los detalles y restricciones relacionados. Esto puede causar que el Modelo del Dominio sea sujeto de interpretaciones subjetivas que conlleven a errores de implementación más adelante. Este artículo presenta una forma de reducir la ambigüedad en el Modelo del Dominio mediante el uso de especificaciones formales ligeras en VDM++. A modo de ejemplo, presentamos la especificación formal de un electrocardiógrafo digital. La especificación está basada en la descripción de las características del funcionamiento del electrocardiógrafo. Se pone especial atención en las características de la captura de la señal electrocardiográfica. Se ha identificado propiedades y restricciones importantes que permiten incrementar la confiabilidad al momento de la implementación. Las propiedades y restricciones se han especificado en forma de invariantes y precondiciones. La validación de la propuesta se realizó con la herramienta VDM++ToolBox.