Fallos informáticos y verificación de programas

PorJosé A. Alonso

Una de las principales aplicaciones del razonamiento automático consiste en la verificación de programas. Por ello, en el comienzo de los cursos de razonamiento automático se suele comentar algunos de los fallos informáticos más famosos.

Una referencia básica sobre fallos informáticos es el libro de Ivars Peterson Error fatal: a la caza de fallos informáticos (publicado por Alianza Editorial en 1999) en el que se comenta algunos errores de programación que tuvieron funestas consecuencias y presenta a alguna de las personas que se dedican a «cazar» estos fallos antes de que provoquen desgracias irreparables.

Otras recopilaciones más recientes de fallos informáticos son las siguientes:

A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con PVS titulado A TCAS-II resolution advisory algorithm.

Sus autores son César Muñoz, Anthony Narkawicz y James Chamberlain (del
Langley Research Center de la NASA en Hampton, EE.UU.).

Su resumen es

The Traffic Alert and Collision Avoidance System (TCAS) is a family of airborne systems designed to reduce the risk of mid-air collisions between aircraft. TCAS II, the current generation of TCAS devices, provides resolution advisories that direct pilots to maintain or increase vertical separation when aircraft distance and time parameters are beyond designed system thresholds. This paper presents a mathematical model of the TCAS II Resolution Advisory (RA) logic that assumes accurate aircraft state information. Based on this model, an algorithm for RA detection is also presented. This algorithm is analogous to a conflict detection algorithm, but instead of predicting loss of separation, it predicts resolution advisories. It has been formally verified that for a kinematic model of aircraft trajectories, this algorithm completely and correctly characterizes all encounter geometries between two aircraft that lead to a resolution advisory within a given lookahead time interval. The RA detection algorithm proposed in this paper is a fundamental component of a NASA sense and avoid concept for the integration of Unmanned Aircraft Systems in civil airspace.

Este trabajo es parte del proyecto de la NASA Airborne Coordinated Resolution and Detection (ACCoRD) que está integrado en el proyecto Formal Analysis of Conflict Detection and Resolution Algorithms.

El trabajo se presentó el 19 de agosto en la AIAA Guidance, Navigation, and Control Conference.

Cero elevado a cero y errores informáticos

PorJosé A. Alonso

Es muy frecuente los errores que se comenten al calcular el valor de “cero elevado a cero”. De esta forma, hay quienes piensan erróneamente que es un operación “prohibida”, que es una indeterminada o que su valor es 0.

En el artículo Cero elevado a la cero de Gustavo Piñeiro se explica detalladamente porqué cero elevado a cero es igual a uno.

Los errores sobre cero elevado a cero no sólo se dan entre los humanos, sino que también se dan en los sistemas informáticos. Maxima lo calcula erróneamente como se puede observar en la siguiente sesión
Read More “Cero elevado a cero y errores informáticos”