Model checking is an existing approach for automatic reasoning. The model checker is an important tool and has been applied to software engineering for system verification. As an extension of model checking, model update is a new concept and has been defined and developed in this dissertation. A model updater is employed as an automatic system modification tool for software verification. The combination of model checking and model update completes the task of automatic system verification. In this dissertation, a comprehensive theoretical foundation and prototype implementation for CTL model update are developed. First, five primitive updates which capture the basic atomic operations in a CTL Kripke model are identified and formalized. Next, the minimal change criteria for CTL model update based on these primitive operations are defined. Then, updating an original model to a new model satisfying CTL semantics based on previous primitive updates and minimal change rules is characterized. The related complexity of CTL model update is also analyzed. Following this research, formal algorithms in the form of pseudo code to be used as the guidance for future implementation are designed. Then, a prototype CTL model updater is implemented. This prototype CTL model updater is a stand alone utility and contains both model checking and update functions. The prototype is then applied to three well known models and has successfully been tested. During the implementation, as a byproduct, the approach for extracting a complete Kripke model from NuSMV is described. Also, during the implementation, an up-date model explosion problem is discovered and further minimal change rules based on the original minimal change rules are proposed which significantly reduce the number of minimally updated models. The corresponding theory is formalized and the complexity for solving the update model explosion problem is analyzed. / Doctor of Philosophy (Ph.D.)
| Identifer | oai:union.ndltd.org:ADTP/181735 |
| Date | January 2007 |
| Creators | Ding, Yulin, University of Western Sydney, College of Health and Science, School of Computing and Mathematics |
| Source Sets | Australiasian Digital Theses Program |
| Language | English |
| Detected Language | English |
Page generated in 0.0025 seconds