Abstract

Software-intensive systems have become extremely complex and susceptible to defects and vulnerabilities. At the same time, the consequences of software errors have also become much more severe. In order to reduce the overall development cost and assure the security and reliability of the final product, it is of critical importance to investigate techniques able to detect defects as early as possible in the software development process, where the costs of repairing a software flaw are much lower than at the maintenance phase. In this research work, we propose an approach for detecting flaw at the design phase by combining two highly successful techniques in the information technology (IT) industry in the field of modeling languages and verification technologies. The first one is the Unified Modeling Language (UML). It has become the de facto language for software specification and design. UML is now used by a wide range of professionals with very different background. The second one is Model Checking , which is a formal verification technique that allows the desired properties to be verified through the inspection of all possible states of the model under consideration. Despite the fact that Model Checking gives significant capabilities to developers in order to create a secure design of the system, they are still not very popular in the UML community. There are many challenges faced by UML developers when it comes to combine UML with model checking (e.g., developer are not familiar with formal logics, the verification result is not in the UML notation, and the generation of the model checkers code from UML models is a problematic task). The proposed approach addresses these problems by implementing a new verification framework with support to property specification without using the complexity of formal languages, UML-like notation for the verification results, and a fully automatic verification process