Reseña: Formal specification and verification of well-formedness in business process product lines

PorJosé A. Alonso

Se ha publicado un nuevo trabajo de razonamiento formalizado en PVS: Formal specification and verification of well-formedness in business process product lines.

Sus autores son Giselle Machado, Vander Alves y Rohit Gheyi.

El trabajo se presentará el 23 de septiembre en el LA-WASP 2012 (6th Latin-American Workshop on Aspect-Oriented Software Development).

Su resumen es

Quality assurance is a key challenge in product lines (PLs). Given the exponential growth of product variants as a function of the number of features, ensuring that all products meet given properties is a non-trivial issue. In particular, this holds for well-formedness in PLs. Although this has been explored at some levels of abstraction (e.g., implementation), this remains unexplored for business process PLs developed using a compositional approach. Accordingly, in this paper we report on-going work in formalizing Business Process Product Lines, including the definition of well-formedness rules, formal specification of transformations, and the proof that transformations preserve well-formedness without having to instantiate all variants. Formalization and proofs are provided in the Prototype Verification System, which has a formal specification language and a proof assistant.

El código de la formalización en PVS se encuentra aquí.

Reseña: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization

PorJosé A. Alonso

Esta semana se ha publicado en el Journal of Automated Reasoning un nuevo artículo de razonamiento formalizado en PVS: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization. Una versión previa se puede leer libremente aquí.

Los autores son César Muñoz y Anthony Narkawicz de NASA Langley Formal Methods.

Su resumen es

This paper presents a formalization in higher-order logic of an efficient representation of multivariate Bernstein polynomials. Using this representation, an algorithm for finding lower and upper bounds of the minimum and maximum values of a polynomial has been formalized and verified correct in the Prototype Verification System (PVS). The algorithm is used in the definition of proof strategies for formally and automatically solving polynomial global optimization problems.

Reseña: A framework for formally verifying software transactional memory algorithms

PorJosé A. Alonso

Se ha publicado un nuevo artículo de verificación con PVS:
A framework for formally verifying software transactional memory algorithms que se presentará el 3 de Septiembre en CONCUR 2012 (23rd International Conference on Concurrency Theory).

Sus autores son Mohsen Lesani, Victor Luchangco y Mark Moir. El primero trabaja en UCLA y los restantes en Oracle.

El resumen del artículo es

We present a framework for verifying transactional memory (TM) algorithms. Specifications and algorithms are specified using I/O automata, enabling hierarchical proofs that the algorithms implement the specifications. We have used this framework to develop what we believe is the first fully formal machine-checked verification of a practical TM algorithm: the NOrec algorithm of Dalessandro, Spear and Scott.

Our framework is available for others to use and extend. New proofs can leverage existing ones, eliminating significant work and complexity.

Reseña: Compositional verification of a communication protocol for a remotely operated aircraft

PorJosé A. Alonso

La semana pasada se publicó un nuevo artículo de verificación formal con PVS: Compositional verification of a communication protocol for a remotely operated aircraft.

Los autores del artículo son Alwyn E. Goodloe and César A. Muñoz.

El resumen del artículo es

This paper presents the formal specification and verification of a communication protocol between a ground station and a remotely operated aircraft. The protocol can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process should satisfy a distinct delivery requirement. A compositional technique is used to formally prove that the protocol satisfies these requirements. Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.

En la Red se publicó una versión preliminar del artículo.

ProofWiki y la verificación de las demostraciones matemáticas

PorJosé A. Alonso

ProofWiki es un compendio de demostraciones matemáticas escritas de manera colaborativa en una wiki. Su objetivo es colecionar y clasificar demostraciones de teoremas matemáticos.

El proyecto empezó en marzo de 2008 y actualmente incluye 2.804 demostraciones escritas por sus 297 usuarios. Las demostraciones se encuentran clasificadas en 34 categorías. Una de las categorías particularmente interesante es la de teoremas con nombres en la que aparecen 247 teoremas. También es interesante la página de los teoremas más populares según el número de visitas.

ProofWiki podría servir de base para otro proyecto cuyo objetivo final fuese la verificación formal de las demostraciones matemáticas. Para ello se podría crear una wiki y, de forma colaborativa, escribir las verificaciones de las demostraciones de ProofWiki usando los distintos sistemas de razonamiento asistido por ordenador (como Isabelle/HOL/Isar, PVS, ACL2, Coq, HOL, HOL Light o Mizar).