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: Proving the impossibility of trisecting an angle and doubling the cube

PorJosé A. Alonso

Se ha publicado en The Archive of Formal Proofs un nuevo trabajo de razonamiento formalizado en Isabelle sobre geometría: Proving the impossibility of trisecting an angle and doubling the cube.

Sus autors son Ralph Romanos y Lawrence Paulson (de la Universidad de Cambridge).

Su resumen es

Squaring the circle, doubling the cube and trisecting an angle, using a compass and straightedge alone, are classic unsolved problems first posed by the ancient Greeks. All three problems were proved to be impossible in the 19th century. The following document presents the proof of the impossibility of solving the latter two problems using Isabelle/HOL, following a proof by Carrega. The proof uses elementary methods: no Galois theory or field extensions. The set of points constructible using a compass and straightedge is defined inductively. Radical expressions, which involve only square roots and arithmetic of rational numbers, are defined, and we find that all constructive points have radical coordinates. Finally, doubling the cube and trisecting certain angles requires solving certain cubic equations that can be proved to have no rational roots. The Isabelle proofs require a great many detailed calculations.