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.

Formal verification of cryptographic security proofs

PorJosé A. Alonso

Se ha publicado una tesis de verificación formal con Isabelle/HOL titulada Formal verification of cryptographic security proofs.

Su autor es Matthias Berg (de la Universidad de Sarre (en alemán: Saarland)) dirigido por Michael Backes.

Su resumen es

Verifying cryptographic security proofs manually is inherently tedious and error-prone. The game-playing technique for cryptographic proofs advocates a modular proof design where cryptographic programs called games are transformed stepwise such that each step can be analyzed individually. This code-based approach has rendered the formal verification of such proofs using mechanized tools feasible.

In the first part of this dissertation we present Verypto: a framework to formally verify game-based cryptographic security proofs in a machine-assisted manner. Verypto has been implemented in the Isabelle proof assistant and provides a formal language to specify the constructs occurring in typical cryptographic games, including probabilistic behavior, the usage of oracles, and polynomial-time programs. We have verified the correctness of several game transformations and demonstrate their applicability by verifying that the composition of 1-1 one-way functions is one-way and by verifying the IND-CPA security of the ElGamal encryption scheme.

In a related project Barthe et al. developed the EasyCrypt toolset, which employs techniques from automated program verification to validate game transformations. In the second part of this dissertation we use EasyCrypt to verify the security of the Merkle-Damgård construction – a general design principle underlying many hash functions. In particular we verify its collision resistance and prove that it is indifferentiable from a random oracle.

Polygonal numbers in Mizar

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Mizar titulado Polygonal numbers in Mizar.

Su autor es Adam Grabowski (de la Universidad de Białystok, Polonia).

Su resumen es

In the article the formal characterization of triangular numbers (famous from [14] and words “EYPHKA! num = ∆ + ∆ + ∆”) [16] is given. Our primary aim was to formalize one of the items (42) from Wiedijk’s Top 100 Mathematical Theorems list, namely that the sequence of sums of reciprocals of triangular numbers converges to 2 and this Mizar representation was written in 2007. As the Mizar language evolved and attributes with arguments were implemented, we decided to extend these lines and we characterized polygonal numbers.

We formalized centered polygonal numbers, the connection between triangular and square numbers, and also some equalities involving Mersenne primes and perfect numbers. We gave also explicit formula to obtain from the polygonal number its ordinal index. Also selected congruences modulo 10 were enumerated. Our work basically covers the Wikipedia item for triangular numbers and
the Online Encyclopedia of Integer Sequences (http://oeis.org/A000217).

An interesting related result [15] could be the proof of Lagrange’s four-square theorem or Fermat’s polygonal number theorem [30].

El artículo se publicará en la revista Formalized Mathematics.

A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle.

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

A Isabelle/HOL formalisation of Gödel’s two incompleteness theorems is presented. Aspects of the development are described in detail, including two separate treatments of variable binding: the nominal package and de Bruijn indices. The work follows Świerczkowski’s a detailed proof, using hereditarily finite set theory.

The machine proofs are fairly readable, thanks to the structured Isar proof language, and concise at under 14,000 lines for both theorems. The paper presents highlights of the proof, commenting on the advantages and disadvantages of the nominal framework and HF set theory. The proof reported here closely follows a detailed exposition by Świerczkowski. His careful and detailed proofs were indispensable, but significant deviations proved to be necessary. For the first time, we have complete, formal proofs of both theorems. They take the form of structured Isar proof scripts that can be examined interactively.

The total proof length of 14000 lines comprises 5000 lines for the second theorem and 9000 lines for the first. (One could also include 3000 lines for HF set theory itself, but then we may as well also count the standard libraries of natural numbers.)

This project took approximately one year, in time left available after fulfilling a Professor’s usual teaching and administrative duties. The underlying set theory took only two weeks to formalise. The Gödel development up to the proof formalisation condition took another five months. From there to the first incompleteness theorem took a further two months, mostly devoted to proving single valued properties. Then the second incompleteness theorem took a further four months, including much time wasted due to misunderstanding this perplexing material.