文章基本信息

标题："CTL Model Update for System Modifications",
本地全文：下载
作者：Y. Zhang ; Y. Ding
期刊名称：Journal of Artificial Intelligence Research
印刷版ISSN：1076-9757
出版年度：2008
卷号：31
页码：113-155
出版社：American Association of Artificial
摘要：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.