Please use this identifier to cite or link to this item:
|Scopus||Web of Science®||Altmetric|
|Title:||CTL model update for system modifications|
Ding, Yulin (Rena)
|Citation:||Journal of Artificial Intelligence Research, 2008; 31:113-155|
|School/Discipline:||School of Computer Science|
|Abstract:||Model checking is a promising technology, which has been applied for verification of many hardware and software systems. In this paper, we introduce the concept of model update towards the development of an automatic system modification tool that extends model checking functions. We define primitive update operations on the models of Computation Tree Logic (CTL) and formalize the principle of minimal change for CTL model update. These primitive update operations, together with the underlying minimal change principle, serve as the foundation for CTL model update. Essential semantic and computational characterizations are provided for our CTL model update approach. We then describe a formal algorithm that implements this approach. We also illustrate two case studies of CTL model updates for the well-known microwave oven example and the Andrew File System 1, from which we further propose a method to optimize the update results in complex system modifications.|
|Rights:||© 2008 AI Access Foundation. All rights reserved.|
|Appears in Collections:||Computer Science publications|
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.