CTL Model Update for System Modifications

TL;DR

This paper introduces a formal method for updating CTL models to facilitate automatic system modifications, ensuring minimal change and providing algorithms and case studies for practical application.

Contribution

It formalizes primitive update operations and the principle of minimal change for CTL model updates, along with algorithms and case studies.

Findings

Defined primitive update operations for CTL models

Developed a formal algorithm for CTL model updates

Demonstrated effectiveness through case studies

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.