A Case Study for CTL Model Update

Abstract. Computational Tree Logic (CTL) model update is a new system modication method for software verication. In this paper, a case study is described to show how a prototype model updater is imple-mented based on the authors ' previous work of model update theoret-ical results [4]. The prototype is coded in Linux C and contains model checking, model update and parsing functions. The prototype is applied to the well known microwave oven example. This case study also illus-trates some key features of our CTL model update approach such as the ve primitive CTL model update operations and the associated minimal change semantics. This case study can be viewed as the rst step towards the integration of model checking and model update for practical system modi cations.