Uma abordagem de dois níveis baseada em verificação de modelos de uma lógica modal para auxiliar na análise de conformidade arquitetural de software

Abstract

Formal methods are fundamental to ensure that software systems behave as expected. These methods are used to identify errors in system design and to certificate that systems follow the proper requirements. In Software Engineering, preserving the correspondence between the design architecture and the architecture indeed implemented by software developers is a crucial issue. Architecture Conformance Checking is the process of checking if these two architectures are in accordance along the software development course. We propose a Model Checking based method to aid Architecture Conformance Checking, which is a fundamental analysis to ensure software quality, dependability and maintainability. In this work, a new logic, which combines temporal logic, hybrid logic and a new logical operator in order to formalize software specifications, is proposed. The method described in this paper uses two structures, namely call graphs and software version graphs. The first one is used to check specifications related to classes and methods and we apply it intending to analyze a specific software version. The latter one gives us an overview of the software development process and we employ it to check global software requirements. These two graphs allow us to design a two-level checking method. The first level deals with specifications of a single software version that must be inspected in the call graph. The second level handles the global requirements throughout all software versions. Using our new operator and a function, we are able to use the same logic in both levels, allowing them to communicate with each other and handle the verification process in a neat and uniform manner. Our two-level approach is the great differential of this work, since the current approaches available in the literature focus on an unique software version at a time. We also present an algorithm, which has polynomial time complexity, to perform Model Checking for our proposed temporal logic.