¿Qué es la Especificación Formal?

    La especificación formal es un área de investigación cuyo propósito es el desarrollo de técnicas, lenguajes y herramientas (basadas en lógicas clásicas y no clásicas, álgebras o cálculos) para alcanzar una de las principales metas de la ingeniería de software: permitir la construcción de sistemas que operen confiablemente a pesar de su complejidad. Aún cuando la aplicación de métodos formales no garantiza la correctitud a priori de un sistema, facilita considerablemente el análisis de las propiedades del sistema, mostrando posibles inconsistencias, ambigüedades o incompletitudes que de otra forma pasarían desapercibidas

    El desarrollo de métodos formales se concreta en la creación de herramientas (FT) las cuales podemos caracterizar rugosamente de la siguiente manera:

    FT $ = $ Lenguaje Formal (LF) $+$ Inferencia mecánica (IM)
    El lenguaje formal se fundamenta ya sea en alguna lógica, cálculo ó en un álgebra, con una sintaxis y semántica determinadas. El lenguaje permite expresar propiedades de un dominio matemático (DM) de manera clara y no ambigua. La amplitud del dominio DM establece la capacidad expresiva del lenguaje. Un LF puede estar completamente basado en la lógica, álgebra ó cálculo que lo sustenta ó tratarse de un fragmento sintáctico (i.e. un subconjunto preferencial) dentro del cual se puedan expresar propiedades útiles.

    La parte de inferencia mecánica se refiere al sustento operacional, generalmente en términos de la teoría de pruebas para una lógica, u operaciones de reducción en un álgebra. Se pretende que las propiedades fundamentales de un sistema que están siendo modeladas por el LF puedan ser demostradas: la construcción de pruebas formales constituye el vehículo principal para reflejar las propiedades del sistema que está siendo modelado, identificando posibles errores de diseño, inconsistencias, etc. Y más aún, la construcción de pruebas se vuelve trascendente cuando permite definir paradigmas abstractos de cómputo: cómputo como reducción de pruebas y cómputo como búsqueda de pruebas. En particular, para cuando el LF está fundamentado en una lógica, su IM se basa en un demostrador automático de teoremas que puede o no estar apoyado por un constructor de modelos.

    Bajo éste punto de vista, una Especificación Formal no es más que una teoría construída sobre el LF y cuyas propiedades son sustentadas mediante pruebas formales (fig. 1).

    \begin{figure}\setlength {\unitlength}{4144sp}%\begingroup\makeatletter\ifx\S......i\'on de}}\put(3601,-511){\makebox(0,0)[lb]{Pruebas}}\end{picture}\end{figure}
    Figura 1: Concepción operacional de una herramienta formal (FT) que hace las veces de un compilador interactivo el cual recibe como entrada una especificación (teoría) de un sistema escrita en el correspondiente LF, produciendo como salida una serie de análisis (estructurales) semánticos, sustentados por la construcción de pruebas para verificar propiedades del sistema.

    De manera muy similar como ocurre con los lenguajes de programación, la utilidad de una FT está determinada por el equilibrio que ofrezca entre expresividad y desempeño, en particular éste último aspecto está estrechamente ligado con la construcción de pruebas que demuestran las propiedades del sistema, más que respecto al desempeño mismo del sistema modelado. Resulta natural seguir una estrategia experimental: construír prototipos interactivos de LF y sus correspondientes IM para apreciar sus bondades. Sin embargo, esta estrategia tiende a ser subjetiva, pues depende en gran medida de la comodidad que los usuarios sientan por la herramienta.

    Resulta interesante observar que, en general, para un mismo LF se puedan ofrecer varios IM, inclusive que distintos LF (independientemente fundamentados en lógicas, cálculos o álgebras) puedan ser expresivamente equivalentes (atiendan el mismo DM). Se hace patente, por lo tanto considerar un nivel de abstracción superior: poder analizar las propiedades de los LF y de sus IM para identificar equivalencias o correspondencias entre distintos LF (ya sea basados en lógicas, cálculos ó álgebras). Para ello, se debe contar con un metalenguaje que permita expresar a los LF y los IM con la mayor generalidad posible: se considera que ese metalenguaje es la Teoría de Categorías ($\mathcal{TC}$). No obstante, esa generalidad que ofrece la $\mathcal{TC}$ conduce también a establecer consideraciones  pragmáticas, computacionalmente hablando.  Aún cuando la $\mathcal{TC}$ es considerada como demasiado abstracta en el sentido que las estructuras matemáticas son analizadas en tal nivel de generalidad que la realización de cómputos sean posibles o deseables, se tienen antecedentes en su aplicación pragmática para la solución de problemas (que inclusive microsoft admite utilizar!).

    En el campo de las aplicaciones, la emergente tecnología de Agentes computacionales encuentra sitio en prácticamente todo ámbito: desde sistemas operativos distribuidos, lenguajes de programación, dispositivos de hardware, etc. hasta aplicaciones de Inteligencia Artificial, como asistentes personales (interacción humano computadora), comercio electrónico, etc. Las necesidades para asegurar interacción confiable en tales sistemas deben ser satisfechas, por lo que el desarrollo de Métodos Formales encuentra un campo fértil para proponer y desarrollar soluciones a la amplia gama de retos existentes en los sistemas MultiAgente (MAS).
    Tradicionalmente, el uso de métodos formales se toma como una fase separada entre la formulación de análisis y diseño y la implantación y verificación del sistema (fig 2 (a)). Sin embargo, gracias a los modelos de cómputo abstracto que semánticamente pueden sustentarse, es posible que la aplicación de los MF se establezca como una correspondencia partiendo del análisis y conduciendo a la implantación automática y confiable, refinando crecientemente e interactivamente el diseño conforme las necesidades así lo requieran (fig. 2 (b)) o en otras palabras, producir especificaciones eficientemente ejecutables. Es de especial mención los avances en cuanto a la generación semántica de compiladores y máquinas abstractas.

    \begin{figure}\setlength {\unitlength}{4144sp}%\begingroup\makeatletter\ifx\S......no}}\put(451,-466){\makebox(0,0)[lb]{Implantaci\'on}}\end{picture}\end{figure}
    Figura 2: Concepción tradicional (a) de la aplicación de herramientas formales (FT) versus la concepción integral (b).
    Principalmente, el grupo está interesado en las siguientes líneas de investigación:
     
    1. Teoría de Categorías para Meta-análisis de los diferentes formalismos para especificación formal
    2. Aplicación de la Lógica Lineal para la especificación formal de planificación distribuida en sistemas MultiAgente.
  1. Objetivos Generales:
    1. Estudio y análisis de los diferentes formalismos (basados en lógicas, basados en cálculos, basados en álgebras) que se han propuesto para sustentar la especificación, análisis y verificación de sistemas computacionales (secuenciales, concurrentes, distribuidos, empotrados, de tiempo real, etc.).
    2. Como consecuencia de este estudio, es indispensable la experimentación para apreciar la expresividad individual de cada formalismo mediante es el desarrollo de herramientas interactivas (en principio prototipos).
    3. Como necesidad ante la apreciación y comparación experimental, se debe sustentar también una comparación formal de las capacidades de cada formalismo, ya sea alguna lógica matemática, un cálculo ó un álgebra, y por ende de la herramienta construída en base a tal formalismo. Para responder a tal necesidad, pero no restringida a ello, se propone a la Teoría de Categorías como el metalenguaje para sustentar el análisis de los formalismos, comparalos y descubrir propiedades que tendrán repercusión en la implantación computacional eficiente de las herramientas formales correspondientes.