CA901ZE

Vista previa del material en texto

Desafíos y Oportunidades de la Investigación en Métodos Formales 
 
Edgar SERNA M. 
Corporación Universitaria Remington. Facultad de Ciencias Básicas e Ingeniería 
edgar.eserna@remington.edu.co 
Medellín, Colombia. 
 
Alexei SERNA A. 
Instituto Antioqueño de Investigación. Grupo de Investigación CCIS 
alexei.serna@fundacioniai.org 
Medellín, Colombia. 
 
RESUMEN 
 
La investigación teórica y tecnológica en métodos formales ha 
alcanzado recientemente significativos avances, lo que hace 
vislumbrar aplicaciones ambiciosas en las próximas décadas. En 
especial, será posible aplicarlos para apoyar rigurosos y 
coherentes planes de estudio en matemáticas, Ciencias 
Computacionales y algunas ingenierías, a las que se 
incorporarán para verificar hardware, software, algoritmos y 
protocolos, y para el modelado y el diseño de sistemas de 
software complejos. En la industria, se utilizarán para capturar 
requisitos y reglas de negocio, para generar casos de prueba y 
escenarios, para explorar diseños, para verificar protocolos y 
para producir casos seguros. En otras disciplinas científicas y de 
ingeniería se utilizarán para apoyar el modelado y el análisis a 
nivel de sistema. En los próximos años los métodos formales 
tendrán una comunidad de investigación mucho más amplia y 
cubrirán una mayor gama de disciplinas. En este artículo se 
describen los desafíos y oportunidades que debe afrontar la 
investigación en esta área del conocimiento para alcanzar estas 
metas, desde las visiones de la formación, la ciencia y la 
industria. 
 
Palabras clave: Métodos formales, Ciencias Computacionales, 
verificación formal, formación, lógica. 
 
1. INTRODUCCIÓN 
 
Para explicar por qué funcionan o fallan las cosas se 
utiliza argumentos lógicos, pero para verificar la 
correctitud de un producto se utiliza argumentos 
formales, que están conformados por una estructura 
precisa de axiomas y reglas de inferencia. Mediante la 
codificación de estas reglas y utilizando un computador, 
se puede comprobar mecánicamente los argumentos 
formales de una especificación para verificar si es 
correcta. Las técnicas automatizadas de razonamiento 
formal también se utilizan para generar ejemplos de 
algunas limitaciones en matemáticas. El marco 
axiomático ha hecho parte del método científico desde 
Platón y el uso del razonamiento formal ha sido 
defendido desde las investigaciones de Raymond Lully 
[1] y Leibniz [2]. 
 
La investigación en métodos formales ha alcanzado 
significativos progresos en los últimos años, y como 
herramienta y teoría se utilizan cada vez más en una 
amplia variedad de formas en la industria. Muchos de los 
problemas desafiantes en la construcción de sistemas 
software seguros, en la programación de procesadores 
multi-núcleo y en los sistemas ciber-físicos requieren el 
apoyo formal para su modelado y análisis. Po otro lado, 
existe un número creciente de aplicaciones para ellos en 
la investigación en Ciencias Computacionales (CC) y en 
otras disciplinas ingenieriles y científicas. Pero a pesar de 
sus logros y eficiencia demostrada, los métodos formales 
todavía no son una parte integral de los procesos 
formativos en CC, e incluso a nivel de postgrado pocos 
estudiantes siguen carreras de investigación en esta 
tecnología. 
 
En este trabajo se resume algunos de los desafíos que 
enfrentan los métodos formales para lograr una mayor 
utilización y aplicación en los procesos formativos, en la 
ciencia y en la industria, y se describe las oportunidades 
para sus aplicaciones. 
 
2. CONTEXTO DE LOS MÉTODOS FORMALES 
 
Las Ciencias Computacionales se basan en la 
construcción y el estudio de la lógica y la abstracción 
puras. Aunque los computadores existen en la realidad 
física, la computación realmente se encarga de la 
representación y la manipulación de la información, que 
es algo inmaterial. Mientras las matemáticas tratan con 
las leyes de las entidades abstractas, como los números, 
los conjuntos, las superficies, los volúmenes, las 
relaciones, el álgebra y los homomorfismos, la 
computación se focaliza en la manipulación de la 
información representada en abstracciones, como los bits, 
los vectores-bit, las matrices, las tablas, las pilas, las 
colas, los árboles y las bases de datos. Las matemáticas se 
utilizan para representar y analizar la realidad física, pero 
la computación se puede utilizar para el modelado y la 
simulación. Mientras que las primeras tratan con 
operaciones con descripciones concisas, el hardware y el 
software de los sistemas computacionales son 
construcciones complejas. Los sistemas software son 
necesarios para que el hardware se desempeñe con 
precisión y fiabilidad, incluso al tratar con datos poco 
fiables, porque están propensos a fallos de sus 
componentes físicos. 
 
Un científico computacional debe desarrollar la 
capacidad lógico-interpretativa y abstractiva [3] para 
comprender los problemas y modelar las soluciones 
mediante abstracciones, con el fin de especificar 
formalmente los requisitos, construir representaciones de 
datos que sean eficaces y expresivas, diseñar algoritmos 
correctos y eficientes que funcionen con todas las 
entradas posibles, y moldear diseños en un código 
confiable. La lógica y la abstracción son importantes para 
formalizar el entorno en el que el software funcionará, 
para especificar los requisitos, para diseñar e implementar 
la arquitectura del sistema y los componentes, y para 
depurar y mantener el sistema en el tiempo. Estos 
científicos están constantemente solucionando problemas, 
generando representaciones de datos, algoritmos y 
protocolos, diseñando nueva programación y lenguajes 
descriptivos, y resolviendo conflictos de sincronización. 
En los últimos sesenta años las CC han logrado 
desarrollar un cuerpo de conocimientos lógico-abstractos 
para resolver esos problemas, entre los que se encuentra 
los métodos formales. 
 
Los sistemas computacionales tratan con la complejidad a 
todos los niveles, desde las plataformas hardware, los 
protocolos y las representaciones de datos hasta los 
sistemas ciber-físicos y las sofisticadas amenazas a la 
seguridad. Los métodos formales representan un enfoque 
para gestionar esta complejidad mediante el uso de 
representaciones simbólicas de abstracciones, extraídas 
como fórmulas lógicas desde las matemáticas y la 
computación. Estas fórmulas se pueden manipular de 
varias maneras para construir pruebas, a la vez que se ven 
como obstáculos a resolver. La computación trata con 
fenómenos dinámicos en autómatas y máquinas de 
estado, y para capturar el comportamiento y las 
propiedades computacionales se utilizan los formalismos 
expresivos de la lógica temporal. Los métodos formales 
se han desarrollado por más de cinco décadas, desde el 
trabajo pionero de McCarthy [4], y han introducido 
teorías como la programación funcional, la programación 
lógica, la semántica denotacional, la semántica 
operacional, la semántica axiomática, los sistemas tipos, 
la teoría de tipos, la invariancia, la terminación, la 
seguridad, la vida de conexión, la lógica modal, la lógica 
temporal, la lógica descriptiva, los lenguajes de 
especificación, el álgebra de procesos, la interpretación 
abstracta, la verificación en tiempo de ejecución, y otras 
innovaciones conceptuales influyentes. Casi una cuarta 
parte de los premios Turing [5] entregados entre 1966 y 
2007 fueron reconocimientos a trabajos con un 
componente significativo de métodos formales. 
 
Actualmente, el campo de los métodos formales está en 
una encrucijada. En el lado positivo, la tecnología está 
bien desarrollada, existe un amplio número de 
aplicaciones interesantes y de importantes usuarios 
industriales. Sólo en Microsoft Research existe cerca de 
un centenar de investigadores trabajando en el desarrollo 
y uso de los métodos formales. Sin embargo, en el lado 
negativo, no se consideranun componente de la corriente 
principal de las Ciencias Computacionales. Existen pocos 
profesores universitarios trabajando en el área, la oferta 
de cursos a nivel de pregrado o postgrado es escasa, 
difícilmente se desarrollan proyectos importantes, y sólo 
un pequeño número de graduados de doctorado los 
acogen como fuente de investigación y trabajo. Además, 
la capacidad lógico-interpretativa y abstractiva de los 
estudiantes a nivel de pregrado y postgrado y no se 
desarrolla [6], y por el contrario parece haber disminuido 
en los últimos años, a la vez que los planes de estudios en 
CC generan cada vez más fobia hacia cuestiones 
relacionadas con ella y las matemáticas [7]. 
 
La tecnología de los métodos formales es emocionante y 
cada vez más relevante. Con el incremento del poder 
computacional de la última década es el momento de 
llevar las Ciencias Computacionales a la esfera semántica 
de los modelos y la inferencia, lo que posibilitará una 
serie de nuevas aplicaciones en los procesos formativos y 
en la industria. Como por ejemplo en los modelos de 
hardware digital y analógico, las teorías matemáticas, los 
sistemas físicos estáticos y dinámicos, las redes 
biológicas, los sistemas software complejos, e incluso la 
psicología, la filosofía y las interacciones sociales [8]. 
 
La formación a todos los niveles se puede beneficiar del 
modelado y el análisis formal y del uso de metáforas 
computacionales. Actualmente, los procesos formativos 
en diversas áreas se desarrollan en términos de tareas de 
procesamiento de información de bajo nivel, mientras que 
la percepción real se obtiene mediante el uso de modelos 
computacionales y de CC. Por ejemplo, los autómatas 
finitos pueden servir como metáfora para una serie de 
tareas, como el funcionamiento de una máquina 
expendedora, los analizadores de lenguajes, o los 
videojuegos, y los juegos interactivos en sí constituyen 
otra metáfora computacional. Los sistemas dinámicos se 
pueden utilizar para modelar flujos continuos, como los 
vehículos en movimiento, los proyectiles, los niveles de 
fluidos, los reguladores de velocidad, los circuitos 
analógicos y los péndulos. Los sistemas híbridos 
combinan cambios de estados discretos y continuos, y se 
pueden utilizar para termostatos modelo, sistemas de 
control de navegación y sistemas biológicos y 
económicos. Los modelos computacionales, las metáforas 
y la tecnología pueden enriquecer los procesos 
formativos a todos los niveles en las Ciencias 
Computacionales, ya sea mediante el apoyo a la 
formación, el desarrollo de competencias, o la 
colaboración y la comunicación. 
 
La aceptación industrial de los métodos formales también 
se puede ampliar. Actualmente, algunas industrias son 
productoras y consumidoras de herramientas formales. 
Por ejemplo, Intel y AMD los utilizan para controlar la 
equivalencia de circuitos, generar secuencias de prueba, 
controlar modelos de controladores de estado finito, y 
para demostrar teoremas acerca de algoritmos aritméticos 
de punto flotante. Microsoft tiene una serie de proyectos 
que utilizan software de comprobación de modelos y 
razonamiento automatizado para analizar el código 
secuencial para terminación, correctitud asercional y la 
ausencia de vías y callejones sin salida. Rockwell-Collins 
utiliza el razonamiento automatizado para la verificación 
de software. Empresas de diseño electrónico 
automatizado, como Synopsys, Cadence y Mentor 
Graphics, venden herramientas para el control de 
modelos y de equivalencias, y Matlab aplica un 
verificador de diseño Simulink para generar casos de 
prueba y verificar propiedades. Sin embargo, estos 
esfuerzos son relativamente modestos en comparación 
con el uso sistemático que se le puede dar a las 
herramientas formales en cualquiera tipo de proceso. 
 
Aunque la tecnología formal todavía no está lista para 
uso masificado, hoy se tiene un marco amplio para pensar 
en aplicaciones no tradicionales más ambiciosas. Se 
necesita innovaciones audaces que aprovechen la 
potencia de las herramientas y técnicas formales 
modernas para transformar radicalmente los procesos 
formativos, tanto en computación como en otras 
disciplinas que valoran las metáforas computacionales. 
También se tiene una oportunidad para aprovechar los 
métodos formales en el modelado asistido por 
computador y en el diseño de sistemas complejos. 
 
3. COMPONENTES DE LOS MÉTODOS 
FORMALES 
 
La idea de colocar a las matemáticas y a la ciencia sobre 
una base axiomática se remonta a Pitágoras, Platón, 
Aristóteles y Euclides [9]. El uso de un lenguaje formal 
soportado en un razonamiento mecanizado fue defendido 
por primera vez por Raymon Lully en el siglo XIII [1] y 
más tarde por Gottfried Leibniz en el siglo XVII [2]. 
Refiriéndose al uso de la tecnología computacional para 
gestionar grandes volúmenes de información, Vannevar 
Bush [10] sugirió que la lógica puede llegar a ser muy 
difícil, y sin duda sería muy conveniente generar más 
seguridad en su uso. Es posible que algún día hagamos 
clic sobre las opciones operativas de una máquina con la 
misma seguridad que hoy registramos las ventas en una 
caja registradora (p. 12). Hoy, con el incremento de la 
potencia computacional y el desarrollo de potentes 
herramientas software para el razonamiento formal, la 
ciencia está mucho más cerca de alcanzar los objetivos 
que se trazaron estos pensadores visionarios. 
 
La terminación y la invariancia son dos componentes 
importantes de los métodos formales para verificar 
código secuencial. Por ejemplo, considere una bolsa con 
n pelotas blancas y negras y con un suministro ilimitado 
de pelotas por fuera de la bolsa. Partiendo de que existen 
por lo menos dos bolas en la bolsa, el proceso consiste en 
tomar, cada vez, dos bolas de la bolsa e introducir una. Si 
las dos bolas que se toman tienen el mismo color se 
inserta una bola negra, y si es diferente se inserta una 
bola blanca, y así sucesivamente. ¿Es posible asegurar 
que este procedimiento terminará en algún momento? 
¿Qué se puede afirmar acerca del color de la bola que 
queda en la bolsa con respecto al contenido inicial? 
 
Otro ejemplo es el problema del simple recuento de votos 
para determinar si en una elección alguno de los 
candidatos obtuvo la mayoría. La solución propuesta en 
el algoritmo de Boyer y Moore [11] funciona mediante la 
eliminación de pares de votos para candidatos diferentes, 
hasta que los que queden sean para un sólo candidato. El 
otro deberá ser el ganador, si alguien tiene la mayoría. Es 
posible que ninguno de los candidatos obtenga más de la 
mitad de los votos. ¿Por qué funciona este algoritmo? La 
explicación radica en su prueba. En líneas generales, si 
un candidato V tiene mayoría, entonces no importa cómo, 
los votos de V, se aparean y eliminen con los de los otros 
candidatos, porque no habrá votos para V que se queden 
sin pareja. Esta intuición se formaliza tanto en el 
algoritmo como en la prueba, pero en ambos casos los 
detalles de la formalización no son triviales. Estas 
pruebas formalizadas son útiles para descubrir, diseñar e 
implementar algoritmos correctos, así como en la 
demostración de que son correctos. 
 
La semántica formal explica la interpretación matemática 
de un fragmento de texto, o una propiedad del programa, 
y las técnicas de sondeo propuestas para el razonamiento 
acerca de los programas y sus propiedades. Es un pre-
requisito para la aplicación exitosa de los métodos 
formales. La composición es un desafío clave en la 
semántica formal, porque es conveniente desarrollar las 
propiedades de los programas en términos de los sub-
programas constituyentes. Los recientes avances en 
semántica de programas han permitido formalizar su 
comportamiento con almacenamiento dinámico, 
programas orientados a objetos y programas 
concurrentes. 
 
La automatización juegaun rol importante en la 
aplicación exitosa de los métodos formales, debido a que 
para verificar el comportamiento del software y el 
hardware de estado finito se puede utilizar, con una 
cantidad limitada de esfuerzo, la comprobación de 
modelos para anotar los estados con sus propiedades de 
comportamiento. Por ejemplo, para una determinada 
propiedad esto se puede hacer en un tiempo lineal en el 
tamaño del espacio de estado del sistema. Por supuesto, 
ese espacio puede ser enorme, porque incluso un sistema 
con n bits de estado tiene 2n estados posibles. El 
problema de explosión de estados en la comprobación de 
modelos se ha abordado de diversas formas mediante el 
uso de representaciones simbólicas, abstracciones y 
reducciones de orden parcial. 
 
La comprobación de modelos se ha extendido a los 
sistemas de estado infinito, como los paramétricos, los de 
tiempo real y los híbridos lineales. La satisfacibilidad 
booleana mediante la verificación limitada de modelos 
también se utiliza para representar y razonar acerca de 
estos sistemas. En los últimos años se han hecho 
importantes mejoras algorítmicas en estos 
procedimientos, que han sido explotadas por los 
solucionadores de restricciones procedentes de una 
mezcla de teorías, como las de la aritmética, los arreglos, 
los vectores de bits y los tipos de datos recursivos. Los 
procedimientos de satisfacción se pueden utilizar para 
comprobar que una fórmula extensa no se puede 
satisfacer, o para generar contraejemplos, casos de 
prueba, o calendarios, cuando la fórmula en realidad se 
puede satisfacer. 
 
4. DESAFÍOS Y OPORTUNIDADES 
 
En este siglo no existe duda acerca de que los métodos 
formales se deben utilizar más ampliamente en la 
academia y la industria, y muchos de los problemas de 
complejidad que se presentan en la Ingeniería de 
Software moderna, como los relacionados con los 
procesadores de múltiples núcleos, las máquinas virtuales 
múltiples, los requisitos para mayor seguridad y los 
sistemas distribuidos globalmente, no se resuelven 
eficientemente con los métodos existentes, porque son 
densos en las pruebas. También se puede argumentar que 
la formación en Ciencias Computacionales se podría 
beneficiar con la introducción de herramientas y técnicas 
formales al currículo; sin embargo, existen algunos 
desafíos que se deben abordar antes que los beneficios de 
los métodos formales sean un caso convincente. 
 
1. Los lenguajes de programación utilizados en el 
desarrollo de software a gran escala tienen una 
semántica formal compleja. Parte de ella es 
innecesaria e inútil, pero las herramientas formales 
tendrán que hacer frente a la complejidad de 
características como el flujo de información, las 
interrupciones, las discusiones y la concurrencia. 
 
2. La aplicación exitosa de los métodos formales 
requiere habilidad e ingenio, incluso con una 
automatización amplia, pero los usuarios potenciales 
podrían no estar dispuestos a invertir tiempo y dinero 
en una tecnología sin tener una idea clara de los 
beneficios. 
 
3. El costo de la aplicación de los métodos formales en 
un proyecto de desarrollo de software puede ser alto, 
y no se realmente hasta qué punto su aplicación puede 
reducir los costos de las pruebas. 
 
4. Las herramientas formales no son lo suficientemente 
amigables con el usuario como para pensar en un uso 
más amplio. En particular, cuando falla un proceso de 
verificación no se obtiene una respuesta útil; además, 
el mantenimiento de un desarrollo formal es una tarea 
de grandes proporciones, comparable a las del 
mantenimiento de software. 
 
5. Existen diversas herramientas formales eficientes, 
pero a menudo los problemas difíciles requieren una 
combinación de varias de ellas. La interoperabilidad 
es un desafío para estas herramientas, porque 
presentan sutiles diferencias semánticas que se deben 
superar. 
 
La comunidad de investigadores de los métodos formales 
ya han comenzado a trabajar algunos de estos desafíos, y 
mucho de ese esfuerzo tecnológico está orientado para 
hacer que su funcionamiento sea transparente al usuario 
[12]. El costo de la aplicación de los métodos formales 
bajará a medida que las herramientas sean más potentes y 
más integradas. La ley de Moore proporciona una fuerte 
aceleración en el poder de las herramientas formales, y a 
medida que la tecnología se estabiliza el desarrollo de 
interfaces de usuario amigables se convertirá en una 
prioridad. Sea cual sea el futuro, la investigación en 
métodos formales de hoy enfrenta una serie de desafíos, 
los cuales de resumen a continuación. 
 
4.1 En los procesos formativos 
 
Los métodos formales deben estar plenamente integrados 
en la formación de un científico computacional. La 
formación en temas como matemática discreta, lógica 
computacional, teoría de la computación, algoritmos, 
bases de datos, compiladores, sistemas operativos, 
arquitectura de computadores, lenguajes de 
programación, Inteligencia Artificial y análisis numérico 
se puede lograr con mayor eficacia si se utilizan métodos 
y herramientas de modelado y análisis formal. Estos 
cursos carecen actualmente de formalidad, y los 
programas en Ciencias Computacionales e Ingeniería son 
cada vez más alérgicos a las matemáticas. Esto significa 
que los egresados de estos programas no están 
significativamente mejor calificados, en áreas como la 
lógica y la abstracción, de lo que están los egresados en 
otras disciplinas. Existen algunos esfuerzos preliminares 
en esta dirección, como el uso de herramientas para la 
formación en Ingeniería de Software y en pruebas 
formales, que están dando resultado; la propuesta de 
Wing [13] puede servir como modelo para la 
incorporación en los cursos de computación e ingeniería 
de los métodos formales y las herramientas de 
verificación; el proyecto TeachScheme! [14] experimenta 
con el demostrador de teoremas ACL2, para formar a 
estudiantes de primer año en programación; además, 
herramientas como Alloy y Coq se aplican con buenos 
resultados en procesos formativos en Ingeniería de 
Software. 
 
Otras disciplinas también se pueden beneficiar de la 
utilización de los métodos formales. Debido al éxito de la 
verificación formal del hardware, los estudiantes de 
ingeniería eléctrica y electrónica están cada vez más 
necesitados de aplicar el razonamiento booleano y la 
lógica temporal. Muchos cursos de ingeniería utilizan el 
framework de MATLAB en el modelado y la simulación. 
Estos modelos son formalizables y a partir de la 
integración del razonamiento y la simulación se puede 
lograr muchos beneficios pedagógicos. Mathematica es 
una herramienta popular para el álgebra computacional y 
un medio para desarrollar cursos [15, 16], que junto a 
otros sistemas de álgebra computacional se pueden 
mejorar para el desarrollo de pruebas, como se ha hecho 
con REDLOG [17]. La combinación del modelado, la 
construcción de pruebas y las herramientas de álgebra 
computacional puede sustituir a los libros de texto por 
livebooks, que combinen la información con el software 
para apoyar la experimentación, la visualización y la 
prueba. Las herramientas de abstracción que se aplican 
durante un curso determinado pueden llegar a hacer parte 
de las herramientas cotidianas del estudiante. 
 
 
4.2 En la ciencia 
 
Los modelos formales y las técnicas de análisis se 
utilizan en algunas ciencias para lograr la comprensión a 
nivel de sistema. Por ejemplo, las redes reguladoras de 
genes se pueden modelar como redes booleanas, sistemas 
híbridos, o sistemas estocásticos, y utilizando la 
deducción y la verificación de modelos se puede analizar 
sus propiedades. La iniciativa de Systems X [18] logra 
una visión de diferentes procesos naturales y artificiales a 
nivel de sistema. Estos modelos capturan algunas 
abstracciones del sistema destino real utilizando 
máquinas de estadoy limitaciones. Las técnicas formales 
se pueden utilizar para deducir las propiedades de estos 
modelos, y el análisis para las teorías de prueba, el 
diagnóstico de problemas y para hacer predicciones. 
 
4.3 En la industria 
 
Microsoft cuenta con cerca de un centenar de 
investigadores que trabajan en métodos formales. Otras 
compañías tecnológicas, como Intel, AMD, Rockwell 
Collins y The MathWorks, desarrollan y utilizan 
activamente herramientas formales. Algunos proveedores 
de automatización de diseño electrónico, como Cadence, 
Mentor Graphics y Synopsys, cuentan con importantes 
productos de verificación formal en su suite de 
herramientas. Microsoft trabaja en cerca de una decena 
de grandes proyectos en desarrollo formal de 
herramientas de Ingeniería de Software, para la 
especificación, la notación, la generación de pruebas, la 
verificación de modelos y la comprobación de seguridad, 
y varios se centran en la construcción de un motor para 
deducir y explorar modelos simbólicos. Se necesitan 
herramientas en dominios con estrictos requisitos de 
seguridad, mientras que las automatizadas se pueden 
insertar en entornos de desarrollo integrados IDEs y en 
compiladores. Un desafío particular para los métodos 
formales es el desarrollo de sistemas ultra-grandes, los 
cuales integran componentes de software y de hardware 
desde diversas fuentes. 
 
Con la creciente conciencia en las capacidades de las 
herramientas formales y de requisitos más estrictos en 
fiabilidad y seguridad, es posible esperar que la 
implementación de los métodos formales en la industria 
se incremente. También se espera que los laboratorios de 
investigación industrial logren importantes resultados de 
investigación, así como en prototipos. 
 
5. CONCLUSIONES 
 
Las décadas entre 1975 y 2005 se pueden considerar 
como la época dorada de la investigación en métodos 
formales. El trabajo de estos años produjo una serie de 
avances significativos en lógica y semántica de 
programas, lenguajes de especificación y programación, 
metodologías de diseño, técnicas de análisis estático, 
razonamiento automatizado, herramientas de verificación 
de modelos y asistentes de prueba interactivos. Se espera 
que en los próximos decenios la tecnología de los 
métodos formales expanda su campo de aplicación y 
audiencia, tal como se observa la tendencia actual [8]. 
Pero se espera: 1) que estas técnicas sean lo 
suficientemente potentes para ser utilizadas sin ningún 
tipo de esfuerzo intelectual manifiesto y 2) que la 
complementariedad entre la percepción y el juicio 
humano, y el cálculo soportado en computador y la 
inferencia se puedan aprovechar como herramientas clave 
en la gestión de la complejidad de la información. Se 
puede esperar que los métodos formales enriquezcan no 
sólo las Ciencias Computacionales sino otras disciplinas, 
las cuales se beneficiarán de la formalización y de la 
inferencia. 
 
Uno de los desafíos más importantes para la investigación 
en métodos formales será lograr impactar suficientemente 
los programas de formación, tanto a nivel de pregrado 
como de postgrado. Actualmente ya no es secreto que se 
necesitan más profesionales en Ciencias 
Computacionales y en Ingeniería, con una capacidad 
lógico-interpretativa y abstractiva lo suficientemente 
desarrollada como para presentar soluciones eficientes y 
eficaces a los complejos problemas de este siglo. Una 
sólida formación en métodos formales, matemática y 
lógica es la clave para superar este desafío. La esperanza 
es que se logré pronto materializar el sueño de Leibniz: 
de que en lugar de recurrir a argumentos técnicos seamos 
capaces de sentarnos frente a un computador y decir: 
Vamos a calcular. 
 
6. REFERENCIAS 
 
[1] Waite, A. E. (2010). Raymund Lully The Illuminated 
Doctor Of Majorca. Kessinger Publishing. 
[2] Bennett, J. (2003). Learning from Six Philosophers: 
Descartes, Spinoza, Leibniz, Locke, Berkeley, Hume. 
Oxford University Press. 
[3] Serna, M. E. (2012). El Desarrollo de la Capacidad 
Lógico-Interpretativa y Abstractiva. Reporte Técnico: 
USBMED-FIDI-ESM-0112. 
[4] McCarthy, J. (1959). Programs with Common Sense. 
Online [Feb. 2012]. 
[5] http://amturing.acm.org/ [Jan. 2012]. 
[6] Serna, M. E. (2011). Abstraction as a critical component 
in Computer Science training. Avances en Sistemas e 
Informática, 8(3), pp. 79-83. 
[7] Tucker, A. B.; Kelemen, C. F. & Bruce, K. B. (2001). Our 
curriculum has become Math-Phobic! ACM Sigcse 
Bulletin, 33(1), pp. 243-247. 
[8] Serna M. E. Métodos Formales: Perspectiva y Aplicación 
Futura. En H. Pérez G. et al. (Eds.), III Jornadas de 
Investigación Facultad de Ingenierías JOIN 2011, pp. 64-
68. 
[9] Boyer, C. B.; Merzbach, U. C. & Asimov, I. (1991). A 
History of Mathematics. Wiley. 
[10] Bush, V. (1945). As We May Think. The Atlantic 
Monthly, 1(1-2), pp. 1-18. 
[11] Boyer, R. S. & Moore, J. S. (1981). MJRTY – a fast 
majority vote algorithm. Technical Report 32. Institute for 
Computing Science, The University of Texas. 
[12] Tiwari, A.; Rushby, J. & Shankar, N. 2003. Invisible 
formal methods for embedded control systems. 
Proceedings of the IEEE, 91(1), pp. 29-39. 
[13] Wing, J. M. (2000). Weaving formal methods into the 
undergraduate computer science curriculum. Lecture 
Notes in Computer Science, 1816, pp. 2-9. 
[14] Eastlund, C.; Vaillancourt, D. & Felleisen, M. ACL2 for 
freshmen: First experiences. Seventh International 
Workshop on the ACL2 Theorem Prover and its 
Applications, pp. 1-9. Austin, Texas, Nov. 15-16. 
[15] Kaltofen, E. (1997). Teaching computational abstract 
algebra. Journal of Symbolic Computation, 23(5-6), pp. 
503-515. 
[16] Scott, D. S. (1991). Exploration with Mathematica. En: 
Rashid, R. F. (Ed.), CMU Computer Science: A 25th 
Anniversary Commemorative. Assn for Computing 
Machinery, p. 505-519. 
[17] Dolzmann, A. & Sturm, T. (1997). REDLOG: Computer 
algebra meets computer logic. ACM SIGSAM Bulletin, 
31(2), pp. 2-9. 
[18] http://www.systemsx.ch/ [May 2012].