Reseña: Formal specification and verification of well-formedness in business process product lines
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í.