Especificação e verificação formais de boa-formação em linha de produtos de processo de negócio

Abstract

Um grande desafio em linha de produtos (LPs) é garantir as propriedades dos produtos gerados. Com o crescimento exponencial do número de produtos em função do número de características, assegurar que qualquer produto cumpre uma dada propriedade é um problema não trivial. Em particular, este é um problema válido para verificar a boa-formação em LPs. Embora tenha sido explorado em alguns níveis de abstração (por exemplo, a implementação), este problema permanece inexplorado para a linha de produtos de pro cesso de negócios que foi desenvolvida usando uma abordagem composicional e possui melhor modularidade. Assim, nesta dissertação, tratamos do problema de verificação da boa-formação em Linha de Produtos de Processo de Negócio, incluindo a definição de regras de boa-formação de processos de negócio, especificação formal de transformações composicionais, a análise de exemplos e contraexemplos gerados pelo model checking, e a prova de que transformações preservam as propriedades de todos os produtos sem realmente ter que instanciá-los. Foi realizada uma formalização de linha de produtos de processo de negócio em Alloy coma ferramenta Alloy Analyzer, que possui uma linguagem de especificação formal e um mecanismo de verificaço de propriedades (model checking). Também foram realizadas formalização de linha de produtos de processo de negócio e provas de teoremas no Prototype Verification System (PVS), que tem uma linguagem de especificação formal e um assistente de provas. ___________________________________________________________________________________ ABSTRACT

Quality assurance is a key challenge in product lines (PLs). Given the exponential growth of the number of products depending on 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., implementa-tion), this remains unexplored for business process PLs developed using a compositional approach, which has better modularity. Accordingly, in this dissertation we treat the problem of verification of well-formedness Business Process in Product Line, including the definition of well-formedness rules of business process, formal specification of com- positional transformations, the analysis of examples and counterexamples generated by model checking, and the proof that transformations preserve the properties of all products without having to instantiate all variants. We performed a formalization of business process product line with the Alloy tool Alloy Analyzer, which has a formal specification language and a mechanism for verifying properties (model checking). Also formalization of business process product line and proofs of theorems were provided in the Prototype Verification System, which has a formal specification language and a proof assistant.