|
El pasado mes de febrero se dieron a conocer los galardonados con el premio Turing 2007. Este premio, otorgado por la Association for Computer Machinery (ACM) está considerado como el más prestigioso del campo de la informática y la computación.
Aunque la presentación oficial del premio será el 21 de Junio de 2008, ya se conoce el nombre de las personas en las que recaerá. En esta ocasión, son tres: Edmund M. Clarke, E. Allen Emerson y Joseph Sifakis.
El motivo por el cual se les otorga es premio es "por su papel en el proceso de convertir el Model Checking en una tecnología de verificación altamente efectiva ampliamente adoptada en las industrias del hardware y del software".
El Model Checking es un sistema de verificación formal. En principio, y a pesar de lo que reza la dedicatoria del premio, está orientado principalmente a hardware. En el software, debido a su naturaleza y a otros problemas inherentes que plantea, aunque pueda aplicarse en determinados casos, no tiene tanta utilidad práctica. La técnica consiste básicamente en representar el comportamiento de una pieza de hardware con un grafo dirigido, en el cual, los nodos representan estados del hardware y los arcos transiciones entre ellos. A cada nodo se le asocia una serie de reglas escritas en forma de proposiciones de lógica temporal. La matemática desarrollada por los tres galardonados incluye búsquedas y otros cálculos sobre estos grafos que permiten deducir propiedades acerca del modelo, y por ende, del hardware que está representando. En particular y especialmente, esa matemática debe decirnos de manera automática si el modelo satisface correctamente una serie de requerimientos. Además del funcionamiento básico del modelo, los galardonados están involucrados en el desarrollo de varios tipos de optimizaciones y algoritmos mejorados sobre las técnicas básicas.
Para saber más:
-La página de cada uno de ellos. (en inglés)
-Nota de prensa de la ACM acerca de la concesión del premio y breve descripción profesional de cada uno de los galardonados. (en inglés)
-Model checking en wikipedia en español .
-Model checking en wikipedia en inglés (algo más completo).
-Una introducción al Model Checking en embedded.com. (en inglés)
|