A Two-Level Approach Based on Model Checking to Support Architecture Conformance Checking

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 the general idea of an algorithm, which has polynomial time complexity, to perform Model Checking for our proposed temporal logic.