TY - GEN
T1 - System modification case studies
AU - Ding, Yulin
AU - Zhang, Yan
PY - 2007
Y1 - 2007
N2 - Computation Tree Logic (CTL) model update is an approach for software verification and modification, where the minimal change principle is employed to generate admissible models that represent the corrected software design. In this paper, we apply CTL model update to models based on the well known Andrew File System protocols. We demonstrate the process of model update based on our previous theoretical results, and present a prototype implementation. Our case studies show that our model update system is sound and workable, which can be applied to different complex systems.
AB - Computation Tree Logic (CTL) model update is an approach for software verification and modification, where the minimal change principle is employed to generate admissible models that represent the corrected software design. In this paper, we apply CTL model update to models based on the well known Andrew File System protocols. We demonstrate the process of model update based on our previous theoretical results, and present a prototype implementation. Our case studies show that our model update system is sound and workable, which can be applied to different complex systems.
UR - https://www.scopus.com/pages/publications/37349018610
U2 - 10.1109/COMPSAC.2007.206
DO - 10.1109/COMPSAC.2007.206
M3 - Conference Paper
AN - SCOPUS:37349018610
SN - 9780769528700
T3 - Proceedings - International Computer Software and Applications Conference
SP - 355
EP - 360
BT - Proceedings - 31st Annual International Computer Software and Applications Conference, COMPSAC 2007
T2 - 31st Annual International Computer Software and Applications Conference, COMPSAC 2007
Y2 - 24 July 2007 through 27 July 2007
ER -