Resumen de Especificación, validación y verificación formal de un microscopio efecto-túnel

Joaquín Nicolás Ros , Juan Alcalde, José Ambrosio Toval Álvarez , Aurelio Arenas Dalla-Vecchia

• En este trabajo se presenta la especificación de control y de las actividades implicadas en la realización de topografías de un microscopio efecto túnel que se está desarrolllando en el Departamento de Física de la Universidad de Murcia. El proceso de modelización se muestra a través de la metodología que se ha seguido en la construcción de modelo formal, que incluye la obtención de un modelo funcional de las experiencias seleccionadas, la selección de un lenguaje formal de especificación (OBJ3 en este caso), la obtención del modelo algebraico a partir del diagrama funcional mediante el establecimiento de una serie de reglas, y la construcción propiamente dicha del modelo algebraico, ayudándonos de la notación gráfica AlgChart para representar la jerarquía de módulos. Finalmente se seleccionan las propiedades del sistema a validar, y las operaciones del modelo a verificar, en un ambiente estrictamente formal, haciendo uso del prototipo del sistema obtenido automáticamente.