الفهرس 
The Quest for Software Correctness
Proposed method to translate USE to ALLOYOnly 14 pages are availabe for public view
 |  | from | 133 |  |  |
| | | from | 133 | | |
Abstract
Recently, the Software designs process has clearly become much more sophisticated, thus the integrity of software system designs has gradually become difficult to be verified. For this purpose, the unified modelling language (UML) has been produced to be a standard language for designing software.
Verification and validation of UML models are necessary because some of UML models exhibited behaviours are neither wanted nor expected by the developer, this causes severe problems during runtime. This step is usually done by a model checker.
There are considerable numbers of model checking tools. However, this is usually accomplished by experts who have a good awareness of the model checker language and its construction. That’s why it is necessary for a model validator to work along with the model designer. Thereby achieving the concern of separation accomplishes this step. In this thesis, a bridge has been constructed to tighten the gap between design and analysis processes through the USE2ALLOY tool. This tool can transform a model produced by the designer to a model suitable for conducting automated analysis by the validator.
This thesis presents a study of USE2ALLOY with OCL constraints. The translation allows analysis of UML models via Alloy to identify consistencies in those UML models and search for their instances with minimum effort from the designer. A comparison between this work and other related works has been done. Also, a conclusion has drawn and suggestions produced for future work.