Especificación, validación y verificación formal de un microscopio efecto-túnel
- Clares Rodríguez, Buenaventura (dir. congr.)
Editorial: [Almuñécar?] : Asociación Española de Informática y Automática, [1996]
ISBN: 84-8254-080-7
Ano de publicación: 1996
Páxinas: 445-454
Congreso: Jornadas de Informática (2. 1996. Almuñécar)
Tipo: Achega congreso
Resumo
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.