Please use this identifier to cite or link to this item:
https://hdl.handle.net/2440/45338
Citations | ||
Scopus | Web of ScienceĀ® | Altmetric |
---|---|---|
?
|
?
|
Type: | Conference paper |
Title: | A logic approach for LTL system modification |
Author: | Ding, Yulin (Rena) Zhang, Yan |
Citation: | Foundations of intelligent systems : 15th international symposium, ISMIS 2005 : Saratoga Springs, NY, USA, May 25-28 2005 : proceedings / Mohand-Said Hacid (ed.), 2005. pp.435-444 |
Publisher: | Springer |
Issue Date: | 2005 |
Series/Report no.: | Lecture notes in computer science ; 3488. |
ISBN: | 3540258787 |
Conference Name: | International Symposium on Methodologies for Intelligent Systems (15th : 2005 : Saratoga Springs, NY) |
School/Discipline: | School of Computer Science |
Statement of Responsibility: | Yulin Ding and Yan Zhang |
Abstract: | Model checking has been successfully applied to system verification. However, there are no standard and universal tools to date being applied for system modification. This paper introduces a formal approach called the Linear Temporal Logic (LTL) model update for system modification. In contrast to previous error repairing methods, which were usually simple program debugging and specialized technical methods, our LTL model update modifies the existing LTL model of an abstracted system to correct automatically the errors occurring within this model. We introduce three single operations to represent, update, and simplify the updating problem. The minimal change rules are then defined based on such update operations. We show how our approach can eventually be applied in system modifications by illustrating an example of program corrections and characterizing some frequently used properties in the LTL Kripke model. |
DOI: | 10.1007/11425274_45 |
Published version: | http://www.springerlink.com/content/mnb8ktkww22ukq1b/ |
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.