Please use this identifier to cite or link to this item:
https://ptsldigital.ukm.my/jspui/handle/123456789/513471| Title: | A common modeling language for model checkers |
| Authors: | Pathiah binti Abdul Samat (P33780) |
| Supervisor: | Abdullah Mohd Zin, Prof. Dr. |
| Keywords: | Modeling language Model checkers Computer systems -- Verification |
| Issue Date: | 30-Nov-2012 |
| Description: | In recent years there are extensive use of formal verification tool and techniques to check on the behavior of computer systems. One of these formal verification techniques is model checking that is considered to be the most successful approach for verifying requirements of computer system. There are a number of model checkers that have been developed. Each of the model checkers is based on different input languages and they are suitable for model checking different types of systems. Thus, it is important to choose the right model checker for modeling and verifying a system. However, moving from one model checker to another is not an easy task since a user has to deal with different input languages. The main objective of this research is to provide a common modeling language and tool for model checkers to help users to easily model and specify the properties of a system effectively. Specifically, the objectives of this research are (1) To identify common features of model checkers' input languages; (2) To propose an approach of common modeling language for model checkers; (3) To develop a support tool of model checkers to assist users in modeling task; and (4) To evaluate the suitability of the proposed approach. In this method, to identify common features, four different model checkers are compared by modeling and verifying four different types of systems. The development of the common modeling language is done by studying the most popular modeling tool, especially within the Unified Modeling Language (UML) community, that is the UML statechart. The common modeling language is obtained by extending the statechart into a hierarchical form. Translation rules from the common modeling language to a input language of model checkers are then described. The development of the software tool is developed by using the standard software engineering approach. Finally, the evaluation of the proposed language and tool is conducted with the focus group. There are three major contributions of this study. Firstly, this research has identified the common features amongst the model checkers' input languages. Secondly, the research has proposed a common modeling language based. Thirdly, the research has produced a software tool that could help users in using and applying the model checkers. The evaluation of the language and tool shows that the availability of the language and tool can help to reduce the difficulty in modeling and formalizing properties of a computer system for model checking purposes.,Ph.D |
| Pages: | 269 |
| Call Number: | QA76.76.V47.P347 2012 3 |
| Publisher: | UKM, Bangi |
| Appears in Collections: | Faculty of Information Science and Technology / Fakulti Teknologi dan Sains Maklumat |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| ukmvital_74644+Source01+Source010.PDF Restricted Access | 6.24 MB | Adobe PDF |  View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.