Please use this identifier to cite or link to this item:
https://hdl.handle.net/2440/45334
Citations | ||
Scopus | Web of Science® | Altmetric |
---|---|---|
?
|
?
|
Type: | Conference paper |
Title: | A case study for CTL model update |
Author: | Ding, Yulin (Rena) Zhang, Yan |
Citation: | Knowledge science, engineering and management : first international conference, KSEM 2006, Guilin, China, August 5-8, 2006 : proceedings / Jérôme Lang, Fangzhen Lin, Ju Wang, (eds.), pp.88-101 |
Publisher: | Springer |
Issue Date: | 2006 |
ISBN: | 3540370331 |
Conference Name: | KSEM 2006 (2006 : Guilin, China) |
School/Discipline: | School of Computer Science |
Statement of Responsibility: | Yulin Ding and Yan Zhang |
Abstract: | Computational Tree Logic (CTL) model update is a new system modification method for software verification. In this paper, a case study is described to show how a prototype model updater is implemented based on the authors’ previous work of model update theoretical 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 illustrates some key features of our CTL model update approach such as the five primitive CTL model update operations and the associated minimal change semantics. This case study can be viewed as the first step towards the integration of model checking and model update for practical system modifications. |
Description: | The original publication can be found at www.springerlink.com |
DOI: | 10.1007/11811220_9 |
Published version: | http://www.springerlink.com/content/y32r811102608207/ |
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.